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.

learn more… | top users | synonyms

4
votes
1answer
169 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 ...
12
votes
1answer
529 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) ...
7
votes
5answers
835 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
1answer
275 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 ...
2
votes
1answer
101 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 ...
9
votes
6answers
1k 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 ...
11
votes
0answers
247 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 ...
2
votes
3answers
347 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 ...
5
votes
1answer
188 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 ...
3
votes
0answers
102 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 ...
3
votes
1answer
131 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?
5
votes
2answers
364 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 ...
8
votes
4answers
781 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 ...
2
votes
0answers
69 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 ...
7
votes
0answers
305 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 ...
4
votes
2answers
355 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. ...
4
votes
1answer
190 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 ...
5
votes
3answers
551 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 ...
1
vote
3answers
480 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 ...
1
vote
1answer
603 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 ...
0
votes
0answers
170 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 ...
0
votes
0answers
123 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 ...
4
votes
2answers
242 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 ...
22
votes
15answers
4k 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 ...
3
votes
1answer
559 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 ...
1
vote
2answers
325 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 ...
1
vote
1answer
404 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 ...
2
votes
1answer
736 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 ...
3
votes
1answer
460 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 ...
10
votes
2answers
2k views

Consequences of technically proving anything in Coq (on at least Linux) exploiting a bug? [closed]

Technically, it is possible to prove anything in Coq proof assistant [1] (on at least Linux) due to a programming feature (or bug). This seems tractable when validating large proofs. Human analysis ...
10
votes
1answer
458 views

Left-bracketed Ackermann function also not primitive recursive?

The original Ackermann function $\varphi\colon \mathbb{N}\times\mathbb{N}\times\mathbb{N}_0\to \mathbb{N}$ as defined in [1] was invented to prove that there is a function that is recursive but not ...
7
votes
1answer
326 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 ...
18
votes
8answers
3k views

Proofs of Gödel's theorem

I am interested in different contexts in which Gödel's incompleteness theorems arise. Besides traditional Gödelian proof via arithmetization and formalization of liar paradox it may also be obtained ...
7
votes
2answers
581 views

Ordinal Analysis of Peano Arithmetic with Restricted Induction

If we take Peano Arithmetic and restrict induction to formulas over various fragments of the arithmetic hierarchy, say to the $\Sigma^0_n$ formulas for various $n$ or some other interesting fragments, ...
3
votes
3answers
2k views

About the proof of the proposition “there exists irrational numbers a, b such that a^b is rational”

What does the classical proof of the proposition "there exists irrational numbers a, b such that $a^b$ is rational" want to reveal? I know it has something to do with the difference between classical ...
1
vote
2answers
257 views

Positive & Negative Arity

Hi, You can talk about the arity of a function or an operation - something like addition could have an arity of 2, and negation usually has an arity of 1. A paper I am reading is talking about ...
17
votes
6answers
2k views

Writing “Semi-Formal” Proofs

I am very interested in proofs. I have taken an undergraduate course called "Logic and Set Theory" which I found very interesting, but ultimately unsatisfying. My biggest disappointment has to do ...
8
votes
5answers
2k views

Why is it OK to rely on the Fundamental Theorem of Arithmetic when using Gödel numbering?

Gödel's original proof of the First Incompleteness theorem relies on Gödel numbering. Now, the use of Gödel numbering relies on the fact that the Fundamental Theorem of Arithmetic is true and thus the ...
11
votes
1answer
874 views

Proof theoretic ordinal

In Ordinal Analysis, Proof-theoretic Ordinal of a theory is thought as measure of a consistency strength and computational power. Is it always the case? I. e. are there some general results about ...
1
vote
2answers
595 views

Equational logic

I'm a beginner to this. Can anyone please point me to any resources for studying about equational logic, preferably with some example proofs to wet my feet in? Thanks in advance!
9
votes
2answers
731 views

Asymptotic density of provable statements in ZFC

This question is in response to one of the questions asked here. The OP wanted to know if the percentage of statements provable from ZFC tended to some value, and if so, what it was. In particular, ...
5
votes
4answers
1k views

Zero-knowledge proof that 0 = 1

Suppose one day I came up with a proof that 0 = 1 in some formal system such as PA or ZFC that cannot prove its own consistency (unless it is inconsistent). Would it be possible to have a ...
6
votes
1answer
276 views

Strength of Transfinite Induction on the Difference Hierarchy

I'm wondering if a particular theory of second order arithmetic has been studied or is known to be equivalent to some other theory. Consider the formulas generated by $\Pi^1_1$ and $\Sigma^1_1$ ...
4
votes
5answers
833 views

“Let $x \in A$”, beginning a proof of “$\forall x \in A$ …”, if A were empty [closed]

I work at a four-year teaching school, where we pride ourselves on teaching pure math, proof, and a rather obsessive carefulness of work. Recently I have been criticized for saying that "Let $x \in ...
5
votes
6answers
1k views

Difference between turnstile and implication

Hi, Does anyone know the difference between proving that |- phi ------------------ |- ( psi -> phi ) and proving that ...
4
votes
2answers
348 views

What is the depth of the “provability heirarchy”?

I am not a logician or set theorist, so hopefully this makes sense. Let $T$ be a theory which is expressive enough to make statements like "Statement $A$ has a proof in $T$"; for example, $T$ might ...
-1
votes
5answers
784 views

finding cutting edge papers and books

Hi all, what are the best strategies to find cutting edge papers and books on a field of mathematics? .. Example: 2-3 years ago I had to analyze a time series. I found a paper and showed that to ...
4
votes
3answers
475 views

Can a typing judgment admit essentially different derivations?

In any sort of type theory, there are a bunch of rules for constructing derivations of typing judgments such as $x:A,\; y:B(x) \;\vdash\; z:C(x,y)$. (I intend to include also judgments of the form ...
3
votes
1answer
523 views

Derivability conditions for Robinson arithmetic

Two pieces of hearsay I have encountered about Robinson's Q: Q fails to satisfy the Löb derivability conditions; Pudlák criticised the Löb derivability conditions and suggested rival, weaker ...
23
votes
6answers
3k views

Why can't proofs have infinitely many steps?

I recently saw the proof of the finite axiom of choice from the ZF axioms. The basic idea of the proof is as follows (I'll cover the case where we're choosing from three sets, but the general idea is ...