Questions tagged [proof-theory]

For question in Proof Theory, where "proofs" themselves are the object of mathematical investigation. It is not to be used to request a proof of some result.

Filter by
Sorted by
Tagged with
8 votes
2 answers
552 views

Cut elimination algorithms

Gentzen's Hauptsatz in first order logic includes an algorithm taking any proof in the sequent calculus with cut rule, and delivering a proof without cut rule (and with the subformula property). So ...
Colin McLarty's user avatar
3 votes
0 answers
718 views

The substitution theorem in first order logic (finitely many variables)

We consider the language ${\cal L}=\{\in\}$ with an arbitrary set of variables $V$. Specifically we define ${\bf P}(V)$ as the free algebra of type $\{\bot,\to\}\cup\{\forall x:x\in V\}$ (with the ...
Noel Vaillant's user avatar
2 votes
1 answer
2k views

Hilbert style axiomatic proof or sequent Calculus?

I am puzzling with the question which of the two proof systems (Hilbert style axiomatic proofs or substructural Sequent Calculi) is the most discriminatory? With discriminatory I mean is which proof ...
Willemien's user avatar
  • 305
3 votes
2 answers
151 views

Membership Provability in co-RE Sets

We're interested in recursive predicates $P(n)$ with RE range $R$ and non-RE complement $R^\prime$. For various $n \in R^\prime$ we may be able to prove that $n \in R^\prime$. For instance, if $P$ ...
zz14's user avatar
  • 33
9 votes
1 answer
294 views

The Hasse Minkowski theorem in Peano arithmetic

Harvey Friedman's "Concrete Mathematical Incompleteness" at http://www.math.osu.edu/~friedman.8/pdf/0.Intro061311.pdf cites the Hasse Minkowski theorem saying quadratic forms over a number field are ...
Colin McLarty's user avatar
2 votes
1 answer
389 views

Ordinal Exponentiation in Genzen's Sequent Calculus

For Genzen's sequent calculus with PA axioms, why is the proof-theoretic ordinal $\epsilon_0$? This seems to hinge on what exactly it means for the level of a cut or CJ inference figure to be higher ...
vertigo's user avatar
  • 21
7 votes
1 answer
2k views

Axiomatization of first order logic (finitely many variables)

Standard textbooks in mathematical logic will assume an infinite supply of variables. Their axiomatization of first order logic will typically contain an axiom of the form $\forall x\phi_{1}\to\phi_{1}...
Noel Vaillant's user avatar
2 votes
2 answers
371 views

Embedding of consistent subset in first order logic (finitely many variables)

I am looking at FOL with no equality, no constant, no function symbol and the unique binary predicate $\in$ with variables in arbitrary sets $V$ or $W$. Specifically we define ${\bf P}(V)$ as the free ...
Noel Vaillant's user avatar
14 votes
1 answer
1k views

Reverse mathematics of Hilbert's Theorem 90

What is known, and what is published, on the reverse mathematics of the nest of results called Hilbert's Theorem 90?
Colin McLarty's user avatar
7 votes
7 answers
627 views

Strength of Bishop style constructive mathematics vs $\mathsf{RCA}_0$

This question came out of this other MO question of mine. My question is Is there a formal comparison between $\mathsf{RCA}_0$ and $\mathsf{BISH}$ (Bishop style constructive mathematics as used in ...
Jason Rute's user avatar
  • 6,237
19 votes
1 answer
1k views

Goodstein's theorem without transfinite induction

Goodstein's theorem is an example of a theorem that is not provable from first order arithmetic. All proofs of the theorem seem to deploy transfinite induction and I've wondered if one could prove the ...
user avatar
1 vote
3 answers
298 views

Is there an recursively axiomatized system with infinitely many proofs for some propositions or a proposition [closed]

Is there any recursively axiomized system with infinitely many proofs for some propositions or a proposition? So we will have at least one proposition which is deduced from the recursively axiomatic ...
XL _At_Here_There's user avatar
16 votes
6 answers
4k views

Deduction theorem

Is there an axiomatic system where the deduction theorem does not hold?
Octavio's user avatar
  • 163
7 votes
1 answer
1k views

Is the equivalence between a $\Sigma^0_1$ and a $\Pi^0_1$ formula defining the same recursive set provable in a sufficiently strong arithmetic ?

Let $A$ be a recursive set. $A$ is recursively enumerable, so $A$ may be defined by a $\Sigma^0_1$ formula, i.e. by $\exists \overrightarrow{a} \phi (\overrightarrow{a}, n)$, where $\phi$ contains no ...
Dabs's user avatar
  • 73
11 votes
1 answer
428 views

Does any lower bound on proofs of FLT improve Shepherdson 1965?

In 1965 Shepherdson proved that FLT is independent of the fragment of PA that uses only open induction and signature $0,S,+\times$. Indeed $2x+1\neq 2y$ is independent of that fragment. Schmerl ...
Colin McLarty's user avatar
19 votes
2 answers
3k views

When does $ZFC \vdash\ ' ZFC \vdash \varphi\ '$ imply $ZFC \vdash \varphi$?

Being a new member, I am not yet sure whether my question will be taken as a research level question (and thus, appropriate for MO). However, I have seen similar questions on MO, couple of which led ...
Burak's user avatar
  • 4,115
13 votes
1 answer
845 views

What metatheory proves $\mathsf{ACA}_0$ conservative over PA?

Simpson's book shows $\mathsf{ACA}_0$ is conservative over $\mathsf{PA}$ in the natural way by model theory using definable subsets. Of course, $\mathsf{ACA}_0$ being conservative over PA is ...
Colin McLarty's user avatar
8 votes
1 answer
572 views

Interpretability and consistency strength

I have heard there is some fairly recent result showing that whenever theories $T$ and $T'$ have the same consistency strength, then each can interpret the other. I suppose it refers to first order ...
Colin McLarty's user avatar
14 votes
3 answers
897 views

Reverse mathematics below RCA

I'm sure this is a fairly basic question, but I can't seem to find a solid answer: My primary question is: Is there a reasonably nice subsystem of second-order arithmetic corresponding essentially to ...
Noah Schweber's user avatar
32 votes
1 answer
2k views

Godel on recursion-theoretic hierarchies

At the end of his excellent article, "The Emergence of Descriptive Set Theory" (http://math.bu.edu/people/aki/2.pdf), Kanamori writes: "Another mathematical eternal return: Toward the end of his ...
Noah Schweber's user avatar
9 votes
1 answer
932 views

ERA, PRA, PA, transfinite induction and equivalences

I'm quite sure I don't understand very well the links between proof theoretical ordinals of theories, the axioms of transfinite induction and the objects a theory can prove to exist. For instance I'm ...
Primitive Recursive Fab's user avatar
4 votes
1 answer
272 views

Notation for upperbound power sets.

There is a standard notation $\mathrm{ZF}[n]$ for Zermelo Fraenkel set theory with the power set axiom restricted to saying the set of natural numbers has $n$ successive power sets $\beth_0\dots\...
Colin McLarty's user avatar
29 votes
2 answers
3k views

Does Taranovsky's system of ordinal notations make sense?

Dmytro Taranovsky has a Web page on which he claims to define a system of ordinal notations strong enough to provide an ordinal analysis of full second-order arithmetic. I think (perhaps unjustly) ...
Gro-Tsen's user avatar
  • 29.9k
15 votes
5 answers
3k views

Understanding the nature and structure of proofs; Reverse Mathematics and Proof Theory. Prerequisites? Good introductory texts?

I'm still studying maths at undergraduate level, but intend to continue exploring topics in pure maths after I have graduated, so am thinking already about what directions I'd like to persue now, (as ...
2 votes
1 answer
469 views

Sequent calculus: is there a complete linear reasoning (i.e., no trees)?

In Gentzen's sequent calculus, a formal proof is described by a tree, with each node representing the sequent obtained from the child(ren) by applying a given inference rule. If no inference rule has ...
Marco Caminati's user avatar
1 vote
1 answer
141 views

Role of statistical estimation in formal proof

Consider the following scenario: There is some mathematical constant $c$ that you want to compute. You don't have a formal proof for any particular value of $c$, but you have some sound statistical ...
David Harris's user avatar
  • 3,397
13 votes
6 answers
4k views

Non-constructive proofs vs. efficient algorithms

My question concerns what is meant by "nonconstructive", and whether it has ever been defined in terms of computational complexity. The wikipedia article on constructive proof begins, "a constructive ...
Sam Hopkins's user avatar
  • 22.7k
14 votes
0 answers
482 views

How to measure the strength of Zermelo over bounded Zermelo?

Bounded Zermelo is Zermelo set theory with only bounded separation. It has the same strength as simple type theory or MacLane set theory or ETCS. It is a finitely axiomatized fragment of Zermelo, so ...
Colin McLarty's user avatar
3 votes
3 answers
2k views

Existential instantiation in Hilbert-style deduction systems

In some deduction systems there is a rule* that given $\exists x (\phi(x))$, we can infer $\phi(y)$, where $y$ is a fresh variable (i.e., one we haven't yet mentioned in this context). Call this rule "...
Nick Thomas's user avatar
10 votes
1 answer
691 views

Arithmetic strength of Peano + the Howard ordinal

Consider the theory $\mathrm{PA}+\mathrm{BHO}$ consisting of first-order Peano arithmetic ($\mathrm{PA}$) enriched by an axiom scheme which allows well-founded induction up to any ordinal less than [a ...
Gro-Tsen's user avatar
  • 29.9k
3 votes
0 answers
154 views

Why the choice of pairing function in Subsystems of Second Order Arithmetic?

Simpson's book uses a pairing function $\langle i,j\rangle = (i+j)^2+j$. Is that choice of function simply unimportant, or does it have expository advantages over the Cantor pairing, or does it have ...
Colin McLarty's user avatar
3 votes
1 answer
219 views

Does $\Pi^1_{\infty}$ comprehension imply ATR$_0$?

$\Pi^1_{\infty}\text{-}\mathsf{CA}_0$ proves existence of models of ATR$_0$. But I think it does not imply ATR$_0$, because Axiom Beta is a kind of replacement axiom. Is that right?
Colin McLarty's user avatar
6 votes
2 answers
913 views

Subscript 0 in Reverse Mathematics

What does the subscript 0 mean on terms like $\mathsf{ATR}_0$? Does it mean the same thing in $\Pi^1_k\text{-}\mathsf{CA}_0$? If I frame higher order analogues of these, should I change that ...
Colin McLarty's user avatar
8 votes
4 answers
3k views

How many well orderings of $\aleph_0$ are there?

What is known about the set of well orderings of $\aleph_0$ in set theory without choice? I do not mean the set of countable well-order types, but the set of all subsets of $\aleph_0$ which (relative ...
Colin McLarty's user avatar
2 votes
0 answers
82 views

Seeking name for an order raising operator in Higher Order Arithmetic.

Any class $X$ of order $j$ in HOA is in bijection with the order $j+1$ class built up from singletons $\{x\}$ of natural numbers $x$ just the way that $X$ is built up from the numbers $x$. And of ...
Colin McLarty's user avatar
9 votes
0 answers
396 views

Can second order arithmetic make $\aleph_1^L$ countable?

Simpson's book Subsystems of Second Order Arithmetic shows $Z_2$ can interpret some fragments of ZF strong enough to give good theories of constructible sets and formalize statements like "there is a ...
Colin McLarty's user avatar
5 votes
2 answers
809 views

When are provability predicates provably equivalent?

Fix notation Suppose that $Prf_1(m, n)$ is the numerical relation that holds when $m$ numbers a $T$-proof of the sentence numbered $n$, according to scheme 1 for numbering wffs and sequences of wffs. ...
Peter Smith's user avatar
  • 1,599
5 votes
1 answer
355 views

History of provably total functions of a theory

Provably total functions of an arithmetical theory is one of the tools used in proof theoretic analysis of theories. I am looking for early history of its development. In particular, Where was ...
Kaveh's user avatar
  • 5,362
6 votes
3 answers
1k views

computational complexity of primitive recursive functions

If we have a rewrite system for primitive recursive functions, which simplifies each term according to how the function was defined, then what is the computational complexity of this calculation? That ...
AKS's user avatar
  • 63
1 vote
3 answers
977 views

Applicability of Deduction theorem to Primitive recursive arithmetic [closed]

Hello. I already asked the question here. The main point is that I tried to prove in Primitive recursive arithmetic (PRA) the totality of the Ackerman function, and I found, that the single thing ...
eugepros's user avatar
1 vote
1 answer
2k views

How to explain, that logic is the correct way of describing any system, process, etc? [closed]

Logic is the philosophical study of valid reasoning. Mathematical logic is an extension of symbolic logic (which is extension of formal logic) into other areas, in particular to the study of model ...
Mooncer's user avatar
  • 113
1 vote
0 answers
441 views

subformula property (anchored proofs)

Hello, I would like to ask for some explanation on some property of propositional sequent calculus. The sequent calculus that I use here follows that of Stephen Cook, in "Logical Foundations of ...
michael's user avatar
  • 11
0 votes
0 answers
171 views

Implications of complex solutions of Matiyasevich / Chaitin diophantine polynomials.

This is a shot in the dark: In twf:202, an isomorphism $T\cong T^{7}$ between binary trees $T$ and seven tuples of binary trees T^{7} is mentioned. The argument for this isomorphism starts with the ...
graveolensa's user avatar
4 votes
2 answers
278 views

Is there any literature about inner-replacement rule?

Hello all, If you have a theorem $\vdash \alpha \rightarrow \beta$ and a theorem $\vdash \gamma$ then if $\alpha$ is a sub-expression of $\gamma$, and this sub-expression has an even number of ...
Lucas K.'s user avatar
  • 1,659
33 votes
15 answers
6k views

What's a magical theorem in logic?

Some theorems are magical: their hypotheses are easy to meet, and when invoked (as lemmas) in the midst of an otherwise routine proof, they deliver the desired conclusion more or less straightaway&...
4 votes
1 answer
716 views

Proof system with same complexity as "informal mathematics"?

The Completeness Theorem in first-order logic states that any mathematical validity is derivable from axioms. Hence, any informal mathematical proof (which is rigorous) can be translated into a formal ...
David Harris's user avatar
  • 3,397
0 votes
2 answers
434 views

Would intuitionistic refutation method imply permutation of premisses?

Dear All In the classical refutation method, one searches for a proof of $\Gamma, \lnot A \vdash \bot$ instead of $\Gamma \vdash A$. The method works, i.e. is complete and correct, since it is for ...
user avatar
1 vote
1 answer
491 views

Is forward chaining also a form of focusing?

Dear All Lets restrict ourselfs to logical theories which consist only of formulas $P_1 \supset \quad ... \quad P_n \supset Q$, i.e. propositional horn clauses expressed with implication. Lets only ...
user avatar
2 votes
1 answer
820 views

How establish conversion of cut-free proof into uniform proof?

Dear All Gentzen (*) claimed that through cut-elimination, he can normalize proofs. It is well known that cut-eliminated proofs might still contain some unnecessary noise. I am trying to show that ...
user avatar
3 votes
1 answer
857 views

Feferman's extensional and intensional applications of the method of arithmetization

At the very beginning of Feferman's Arithmetization of metamathematics in a general setting it can be read: The method of arithmetization, as developed by Gödel[10], exploits the possibility of ...
Marc Alcobé García's user avatar

1
4 5
6
7 8