Questions tagged [logic]
Questions related to mathematical logic and its use in computer science
1,035 questions
1
vote
1
answer
71
views
scope of "constant symbol" in tree-format natural deduction
I wanted to develop a tree-format natural deduction of the following tautology.
$$ \exists_{x \in S}(P(x)) \quad \implies \quad ( \forall_{y \in S}(P(y) \implies Q(y)) \implies \exists_{z \in S}(Q(z))...
- 141
1
vote
1
answer
51
views
finding an inhabitant in λC to show tautology $¬(A∨B) ⇒(¬A∧¬B)$
I'm really struggling with this exercise 7.8(b) from Type Theory and Formal Proof.
Give λC-derivations verifying the following tautologies of
constructive logic (hint: use Exercise 7.7 and Section 7....
- 141
0
votes
1
answer
44
views
Repeating a PSPACE problem exponentially many times
I am trying to understand the complexity of a problem that involves solving some $\mathsf{PSPACE}$-complete problem exponentially many times. Namely, one can imagine $\Xi=\{\phi_1,\ldots,\phi_n\}$ to ...
1
vote
1
answer
61
views
finding inhabitant of type corresponding to $\neg(A \land B) \implies (A \implies \neg B)$
Exercise 7.6(c) from Type Theory and Formal Proof (Nederpelt) asks us to derive in λC an inhabitant of a type that corresponds to the following logical statement:
$$\neg(A \land B) \implies (A \...
- 141
0
votes
0
answers
35
views
Turing Machine for postfix Logic Formula
In my Theory of Computability class, our final project is to write a Turing Machine in JFLAP. My project is to write one able to validade a logic formula in postfix notation. So, for example:
input: ...
0
votes
0
answers
26
views
IC3/PDR: Why is $\neg s$ included in the relative induction query?
I am currently trying to understand the IC3/PDR algorithm. My intuitive understanding is that in each iteration, IC3 tries to find a counterexample $c$ (which is a single, concrete state) such that
$c ...
5
votes
1
answer
374
views
help understanding quantifier rules for natural deduction
I'm following this online guide to quantifier inference rules for natural deduction [pdf].
Question: I need help as I don't understand two of the rules, $\forall$-intro and $\exists$-elim. I discuss ...
- 141
3
votes
2
answers
126
views
Is the Law of the Excluded Middle "Or" or "Xor"?
I reading about the Law of the Excluded Middle, that in Classical Logic the following holds for any proposition $P$
$$P \lor \neg P$$
Question: Is that an "OR" or is it an "XOR"?
...
- 141
2
votes
1
answer
185
views
Why does lambda calculus have clear semantics, easy comprehensibility, and serve as a foundation for proof languages?
I'm worried that my question might be ill-posed, but I've tried to formulate it as precisely as possible.
As a computational model, lambda calculus has numerous alternatives, including Turing machines....
- 21
0
votes
0
answers
33
views
logical interpretation of λC type $(S \to S \to *) \to S \to *$
Exercise 6.5 of Type Theory and Formal Proof (Nederpelt) asks us to interpret logically the following judgement:
$$ S : * \quad \vdash \quad \lambda Q : S \to S \to *. \lambda x : S. Qxx \quad : \...
- 395
0
votes
1
answer
109
views
Logical proposition corresponding to the λP type $\Pi x:S.*$?
I'm continuing to work through Chapter 5 of Type Theory and Formal Proof (Nederpelt).
Doing exercise 5.10 I've run into a wall.
I know there is a correspondence between λP types and logical ...
- 395
2
votes
1
answer
416
views
convention for natural deduction proofs when lines are not used
Exercise 5.6 in Type Theory and Formal Proof asks us to first develop a natural deduction proof of the following logical statement (before doing a λP derivation).
$$ (A \implies (A \implies B)) \...
- 395
1
vote
0
answers
55
views
can't find inhabitant of $ \Pi z:A . (\Pi y:(\Pi x:A.B).B) $ in λP
I'm doing ex 5.5 from Type Theory and Formal Proof. Chapter 5 introduces λP, typed dependent on terms, and also the minimal predicate logical equivalents of types.
Ex 5.5 Prove that $A ⇒ ((A ⇒ B) ⇒ B)...
- 395
1
vote
1
answer
91
views
question about proving a tautology via λP (empty context?)
I'm working through Type Theory and Formal Proof (Nederbelt).
Chapter 5 introduces λP (types depending on terms) and takes the first steps in the propositions-as-types and proofs-as-terms.
Simple ...
- 395
2
votes
0
answers
113
views
is there a concept of 'proof-completeness' equivalent to turing completeness
This question comes from curry-howard correspondence.
I am a beginner in this particular topic, i dont yet have much knowledge in proof theory or formal logic or type theory. But as i observed here, ...
- 141