The proof-theory tag has no wiki summary.
12
votes
3answers
330 views
funsplit and polarity of Pi-types
In a recent thread on the Agda mailing list, the
question of $\eta$ laws popped up, in which Peter Hancock made thought-provoking remark.
My understanding is that $\eta$ laws come with negative
...
8
votes
2answers
298 views
Is propositional resolution a complete proof system?
This question is about propositional logic and all occurrences of "resolution" should be read as "propositional resolution".
This question is something extremely basic but it has been bothering me ...
3
votes
1answer
175 views
Why is there a need for cyclic proofs?
I was reading a paper A Generic Cyclic Theorem Prover. This paper explains about automated theorem prover based on various instantiations like the notion of first order logic equations with inductive ...
8
votes
1answer
138 views
Unification-based elimination rule for equality
A few years back, I ran across the following left-rule for equality in sequent calculus:
$$
\frac{s \doteq t \leadsto \theta \qquad
\theta(\Gamma) \vdash \theta(C)}
{\Gamma, s \doteq t ...
2
votes
1answer
146 views
Resolution vs Extended Resolution
Let $R(f)$ and $ER(f)$ be the minimum-size for unsat proofs of $f$ in Resolution and Extended Resolution respectively. What's the best bound we have on $D=\min_f (R(f)-ER(f))$ where $f$ belongs to a ...
12
votes
1answer
221 views
Barendregt's proof of subject reduction for $\lambda2$
I found a problem in Barendregt's proof of subject reduction (Thm 4.2.5 of Lambda calculi with types).
The last step of the proof (page 60), says:
"and hence by Lemma 4.1.19(1), ...
12
votes
3answers
442 views
Can we prove weak normalization for System F by induction on a transfinite ordinal
Weak normalization for the simple typed lambda calculus can be proved (Turing) by induction on $\omega^2$. An extended lambda calculus with recursors on natural numbers (Gentzen) has a weak ...
6
votes
1answer
119 views
converse relationship between the cut rule and the identity axiom
On page 30 of "Proofs and Types" by Girard, Taylor, and Lafont, it is claimed that that the identity axiom for sequent calculus:
C ├ C
has a converse relation with the cut rule:
$$\frac{\vec{A} ...
25
votes
1answer
730 views
Inductive types for large countable ordinal notations.
I'm looking to build notations for large countable ordinals in a "natural way". By "natural way" I mean that given an inductive data type X, that equality should be the usual recursive equality (the ...
11
votes
2answers
260 views
References to programming languages based on conditional logics
Conditional logics are logics which augment traditional logical implication with modal operators corresponding to other notions of condition (for example, the causal conditional $A\; ...
14
votes
1answer
305 views
Looking for papers and articles on the Tarskian Möglichkeit
Some background: Łukasiewicz many-valued logics were intended as modal logics, and Łukasiewicz gave an extensional definition of the modal operator:
$\Diamond A =_{def} \neg A \to A$ (which he ...
16
votes
1answer
489 views
Are types propositions? (What are types exactly?)
I've been reading a lot on type systems and such and I understand roughly why they were introduced (in order to resolve Russel's paradox). I also understand roughly their practical relevance in ...
16
votes
3answers
547 views
How would I go about learning the underlying theory of the Coq proof assistant?
I'm going over the course notes at CIS 500: Software Foundations and the exercises are a lot of fun. I'm only at the third exercise set but I would like to know more about what's happening when I use ...
8
votes
3answers
170 views
Looking for papers and articles on higher-order sequent systems
I am looking for work on systems that are similar to K. Dosen's higher-order sequents ("Sequent Systems for Modal Logic", JSL 50). The only work that I am aware of is recent work by Iemhoff and ...
26
votes
3answers
1k views
Curry-Howard and programs from non-constructive proofs
This is a follow up question to
What is the difference between proofs and programs (or between propositions and types)?
What program would correspond to a non-constructive (classical) proof of the ...
8
votes
2answers
262 views
About the correspondence of left introduction and elimination of implication in Sequent Calculus and in Natural Deduction resp.
Could anyone give an intuitive (not intutionistic) explanation of the correspondence of left introduction and elimination of implication in Sequent Calculus (SC) and Natural Deduction (ND) ...
12
votes
1answer
301 views
Are innermost reductions perpetual in untyped λ-calculus?
(I have already asked this at MathOverflow, but got no answers there.)
Background
In the untyped lambda calculus, a term may contain many redexes, and different choices about which one to reduce may ...
11
votes
2answers
314 views
What happens if we try to extract a witness but it actually does not exist from a term of existential type?
Given a term t : ∀x.∃y.(¬(x = 0) ⇒ x = S(y)) in Martin-Lof's type theory, what's the value of w(t(0)), where ...
