Questions tagged [logic]
Questions related to mathematical logic and its use in computer science
1,036 questions
0
votes
2
answers
91
views
How to "read" the λC encoding of the existential quantifier $\Pi \alpha:*. (\Pi x:S.(Px \to \alpha)) \to \alpha$
The following encodes the existential quantifier in λC, in a context where $S:*, \; P,Q : S \to *$.
$$\Pi \alpha:*. (\Pi x:S.(Px \to \alpha)) \to \alpha$$
I can work through the mechanics showing ...
- 159
2
votes
1
answer
160
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))...
- 159
1
vote
1
answer
58
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....
- 159
0
votes
1
answer
54
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
66
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 \...
- 159
0
votes
0
answers
36
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
27
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
385
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 ...
- 159
3
votes
2
answers
137
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"?
...
- 159
2
votes
1
answer
186
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
111
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
56
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
94
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