Questions tagged [proof-theory]
Questions about analysis of proofs in theories
13
questions
44
votes
4
answers
4k
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 ...
user788
30
votes
3
answers
2k
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 ...
- 21.3k
26
votes
1
answer
1k
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 ...
- 677
16
votes
1
answer
648
views
Relative consistency of PA and some type theories
For a type theory, by consistency, I mean that it has a type which is not inhabited. From the strong normalization of the lambda cube, it follows that system $F$ and system $F_\omega$ are consistent. ...
- 343
16
votes
2
answers
3k
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 ...
- 12.3k
16
votes
3
answers
1k
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 ...
user6892
15
votes
5
answers
616
views
Looking for papers and articles on modal substructural logics
I am looking for papers and articles on modal substructural logics-- not on the semantics of linear logic modalities, but on substructural logics augmented with standard modal operators, e.g. ...
- 815
5
votes
2
answers
866
views
Efficiently modeling Turing machines in Peano Arithmetic
The (undecidable) Peano Arithmetic (PA) is powerful enough to model Turing machines.
Consider a standard first order axiomatization of Peano Arithmetic and a standard Hilbert-style proof system $\...
- 22.3k
2
votes
0
answers
69
views
Is there a relationship between Brown and Palsberg's Self-Interpreter for F-Omega and Lawvere's Fixed Point Theorem?
Brown and Palsberg [0] demonstrated an self-interpreter for F-Omega. To do so, they perform "a careful analysis of the classical theorem [of the impossibility of self-interpretation by total ...
- 83
16
votes
1
answer
551
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 ...
- 163
10
votes
1
answer
308
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 ...
- 31.6k
5
votes
1
answer
99
views
Is there a relation between the techniques used by Dan Willard, versus those of Brown and Palsberg, to exclude diagonalization?
This question extends my inquiry from a previous post [0].
Dan Willard's Self-Justifying Axiom Systems/Self-Verifying Theories [1] and Brown and Palsberg's self-interpreter for F-Omega [2] both employ ...
- 83
0
votes
2
answers
241
views
Why is plus-comm a b $:\equiv$ refl (plus a b) not a proof of the commutativity of addition?
I've been curious about the 'geometric situation' that one has when considering the type
$\prod_{(n,m:\textrm{Nat})}(\textrm{plus}\ n\ m) = (\textrm{plus}\ m\ n)$.
Here, addition is defined in the ...