Questions tagged [proof-theory]

Questions about analysis of proofs in theories

Filter by
Sorted by
Tagged with
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 ...
user avatar
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 ...
user avatar
  • 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 ...
user avatar
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. ...
user avatar
  • 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 ...
user avatar
  • 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 ...
user avatar
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. ...
user avatar
  • 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 $\...
user avatar
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 ...
user avatar
  • 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 ...
user avatar
  • 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 ...
user avatar
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 ...
user avatar
  • 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 ...
user avatar