Questions tagged [proof-theory]

Proof theory is an area of logic that studies proof as formal mathematical objects. If you'd like advice on the presentation of a proof you have in draft, use proof-writing instead. If you'd like feedback on its validity, use proof-verification. If none of the above apply, you do not need a proof-* tag.

Filter by
Sorted by
Tagged with
0
votes
1answer
40 views

Odd perfect number importance [closed]

If someone proved the non existence of an odd perfect number how important would it be to the mathematics field as well as their career?
3
votes
1answer
64 views

First order logic natural deduction problem

I am struggling with a particular case in the (inductive) proof of Theorem 2.8.3 (i) of Logic and Structure by Dirk Van Dalen ($c \neq x$ in the Theorem statement is a variable) The cases when we ...
2
votes
0answers
24 views

Every provably recursive function in PA is bounded by a Hardy function

The following lemma and proof are from Takeuti's Proof Theory (2nd edition, pp. 126-127), I've highlighted the problematic part in blue: How does Takeuti get this inequality? If the proof $x$ is not ...
4
votes
0answers
52 views
+50

Characterization of provably recursive functions in PA

This concerns Takeuti's Proof Theory: the book contains a lot of wonderful material, but the presentation is sometimes lacking (and so many typos!). At least that has been my experience so far, ...
0
votes
1answer
71 views

While using the method of proof by contradiction, are we “assuming” consistency?

I am aware of threads here and here which asks something similar. However, I had something very specific to ask under the same context. I have a very elementary question about the connection between ...
1
vote
2answers
85 views

Help to find a proof in natural deduction

I have a question about the methodology of natural deduction, more specifically finding a proof in natural deduction. The assignment says: Find a proof for the formula $(P \rightarrow \neg P) \...
3
votes
0answers
71 views

Reducing the strength of a category theoretic proof

The motivation for this question is the following: Say we have a formula $\phi$ in peano arithmetic, and we have proof $\pi$ of $\phi$ using possibly higher order arithmetic or category theory (that ...
1
vote
1answer
20 views

A total function is representable iff it is weakly representable

The book A Friendly Introduction to Mathematical Logic - 2nd Edition by Christopher C. Leary and Lars Kristiansen gives the following proposition without proof: Proposition 5.3.6. Suppose that $f$ ...
6
votes
2answers
118 views

Why is finite-ness so important in proofs?

Oftentimes I notice that in proof-writing, something that both my professors and textbook-writers stress is that such-and-such procedure must terminate. Other times, if we want to verify a property is ...
0
votes
1answer
59 views

Proofs checkable by a computer

Propositional logic is decidable, meaning that for every formula we can check whether it is a logical consequence of the theory $T$ (using truth-table method for example). Also we can give a formal ...
3
votes
1answer
45 views

Are theorems in a mathematical theory effectively checkable?

I wonder whether it is possible to effectively check whether some theorem of a mathematical theory (for example group theory) is provable from axioms of that theory. I know that in propositional logic ...
0
votes
0answers
41 views

Does model theory gives a “recipe” for deriving logical consequences from given theory $T$?

Let's suppose classical propositional logic (model theory) and Hilbert's axiomatic system (proof theory). I know that in the Hilbert's axiomatic system there are inference rules for deriving new ...
1
vote
1answer
55 views

Is Halting problem an example of a problem which is true but unprovable?

I have a difficulty understanding Gödel's incompleteness theorems. If it is proven semantically that some problem is undecidable (such as Halting problem), does it means that such a statement is "true ...
0
votes
2answers
44 views

Understanding how to prove either/or type statements in logic

I've been working my way through a logic textbook and I recently came across this problem: B and D are statement forms such that B → D is a tautology. Now, if b and d have no statement letters in ...
1
vote
1answer
42 views

If PA is consistent, for any $n$, does PA prove “$n$ does not code a proof of an inconsistency”?

I am still struggling with the distinction between what is proven where. I think I have a good understanding of the theory and the meta-theory, but then I'm stumped every once in a while, so I fear ...
1
vote
1answer
38 views

What does it mean for two theories to be inter-interpretable?

Mc Larty, is his article "Exploring Categorical Structuralism", gives a proof that the set theory ZFC is inter-interpretable with ETCS+R, a categorical version of set theory. Intuitively, I get the ...
6
votes
0answers
98 views

How many “$Q$-like” sentences are there?

Call a sentence $\varphi$ in the language of arithmetic $Q$-like iff $\mathbb{N}\models\varphi$ and $\{\varphi\}$ is essentially incomplete (= no computably axiomatizable theory containing $\varphi$ ...
2
votes
1answer
80 views

Why use sequents?

In the sequent calculus, the building blocks of a proof are inference rules, which are rules for inferring the validity of certain sequents from other sequents, something like this: $$\frac{\vec\...
5
votes
0answers
166 views

Where did (the language in) this proof of Godel's incompleteness appear?

Many years ago I ran into the following proof of Godel's first incompleteness theorem (here $T$ is an "appropriate" theory of arithmetic.): First, we observe that Tarski's undefinability theorem ...
1
vote
1answer
43 views

Using an inference in an inference

The problem If $\Sigma$ is a set of premises, the Suppes system of inference has the following property (aka deduction theorem) for all propositional formulae $\alpha$ and $\beta$: $$\tag{1}\label{eq:...
0
votes
0answers
51 views

If propositions $P$ and $Q$ are equivalent and $P \implies R$ without using $Q$ is possible, then $Q \implies R$ without using $P$ is possible?

Kind of a weird question. If propositions $P$ and $Q$ are equivalent and if we can show that, for some other proposition $R$, $P \implies R$ without using $Q$, then is there a proof of $Q \implies R$ ...
1
vote
0answers
71 views

Liar sentences and the fixed point theorem

I apologize in advance for the slightly vague nature of this question. If one adds a unary predicate $T$ to the language of arithmetic, one gets a sentence $L$ with the property that $L \...
2
votes
1answer
149 views

Prove $PA\vdash Con_Q$

So let $PA$ be Peano Arithmetic as usual, and $Q$ be Robinson Arithmetic. I'm trying to show that $PA\vdash Con_Q$, i.e. that from $PA$ we can prove $Q$'s consistency. It is assumed that $PA \nvdash ...
3
votes
0answers
78 views

Optimal bound for cost of cut elimination in infinitary logic with transfinite cut-rank in terms of Veblen's $\varphi$ function

The theorem I am referring to is Tait's sharpening of Gentzen's Cut Elimination Theorem in [1], which Schütte [2, p. 204, Theorem 22.8] also calls the ``second cut elimination theorem'' (here written ...
4
votes
2answers
351 views

What is true about a proof system that is complete but not sound?

According to the definitions I have been taught, if a proof system is complete, $\text{If}\ A \Rightarrow B\ \text{then}\ A \vdash B$, and if a proof system is sound, $\text{If}\ A \vdash B\ \text{...
6
votes
0answers
66 views

What is the “validity logic(s)” of moderate theories?

This question is motivated by this old answer of mine. Below, by "appropriate theory" I mean any consistent finitely axiomatizable theory in the language $L_2$ of second-order arithmetic containing $...
2
votes
4answers
255 views

What does discharging an assumption mean in Natural Deduction?

I've also noticed as in the question here that it seems that many references I've read say "discharging an assumption" and assume the reader that we know what that means. It's funny because formal ...
5
votes
0answers
67 views

Calculi for the category theory?

Some branches of mathematics admit calculi with whom one can do syntactical (language-like, grammatical) or geometric operations to arrive at certaing conclusions. The syntactical part (proof theory) ...
3
votes
1answer
47 views

Term existence property for CZF

For Intuitionistic Zermelo Fraenkel (IZF) set theory, Moczydlowski ("Normalization of IZF with Replacements", 2008) proved that the Term Existence Property (TEP) holds, so if $\exists x. \phi(x)$ is ...
1
vote
0answers
54 views

Infinite ordinals in proof theory

I've been trying to get acquainted with proof theory (particularly ordinal analysis) as part of a school project, and am trying to tease out the story behind the appearance of infinite ordinals in a ...
4
votes
1answer
75 views

How many layers of consistency can PA recognize?

$\newcommand{\Cons}{\operatorname{Cons}}\newcommand{\PA}{\mathsf{PA}}$Assuming $\PA$ is consistent, we know that $\PA \nvdash \Cons(\PA)$ and $\PA + \Cons(\PA) \nvdash \Cons(\PA + \Cons(\PA))$, and so ...
1
vote
1answer
76 views

Kurt Schutte Proof Theory (Theorem 1.5 proof)

I had a question regarding the proof of Theorem 1.5 in Kurt Schutte's Proof Theory. Theorem 1.5 If $\mathcal{E}$ is a $P$-form and $V$ a sentential valuation with $VA = t$, then $V \mathcal{E}[A] = ...
2
votes
2answers
68 views

Removing an Antecedent

Suppose $ A \vdash B$ where $A$ is of the form $\forall x\ P(x) \rightarrow \ ... $ and where $B$ does not include the predicate $P$. My intuition is that this implies that $B$ is a tautology, as ...
4
votes
0answers
86 views

self-contained vs. non-self-contained notions of realizability

There seem to be two notions of realizability in literature, where in one case the realization of a formula is fully self-contained with respect to providing a proof object for the given formula, ...
2
votes
1answer
78 views

Proof-theoric ordinal of ETCS

What is the proof-theoric ordinal of Lawvere's elementary theory of the category of sets?
3
votes
3answers
99 views

Theorems & proof by contradiction

The following formula seems to be regarded as the essence of proof by contradiction: p → (q ∧ ~q) ⊢ ~p Or perhaps this one: ~p → (q ∧ ~q) ⊢ p If this is the case, what are the mathematical ...
2
votes
1answer
42 views

Using recursion theory to show a particular sentence is not provable in an extension of PA.

For a natural number $n$, the notation $\underline{n}$ means taking the sucessor of $0$ $n$ times. We denote the Gödel number of a formula $\phi$ by $\lceil \phi \rceil$. We have a function $Sub: \...
0
votes
0answers
30 views

The take lemma needs a coinductive proof

In Are coinductive proofs necessary?, the answerer claimed that we cannot prove inductively the take lemma: Two streams that agree on all initial subsequences of given length are the same. I was ...
0
votes
0answers
23 views

Bourbaki Substitutions in a Theory

From Section 2.3 in Bourbaki's 'Theory of Sets', in the proof of criteria C2 (image attached), Bourbaki asserts that if $\boldsymbol{(T|x)R_k}$ is an implicit axiom in the original theory, then it is ...
3
votes
1answer
79 views

Propositional Logic - How to prove that A implies itself? [duplicate]

I'm trying to form a propositional logic proof chain for the tautology $\delta \implies \delta$, using only the axioms $\alpha \implies (\beta \implies \alpha)$ $((\alpha\implies (\beta \implies\...
2
votes
0answers
49 views

Hilbert calculi for First-Order Logic

I'm a bit confused about the Hilbert-style axiomatization of first-order logic. More precisely, I am a bit confused about completeness w.r.t. to Hilbert-calculi. A complete Hilbert-style calculus I am ...
1
vote
1answer
121 views

Takeuti's proof of the Second Incompleteness theorem

I am reading Gödel's second incompleteness theorem in Takeuti's "Proof theory" (page 85), and I don't understand how he derives the sequent $$ \operatorname{Con},\operatorname{Pr}(\ulcorner A_G\...
0
votes
0answers
36 views

Does the failure of the substitution law of logical equivalents entails inconsistency?

Does the failure of the substitution law of logical equivalents entails inconsistency? By "logical equivalents" I mean equivalences that are logically provable. For example: \begin{equation} \tag{1} (...
3
votes
1answer
65 views

Developing model theory in the language of PA

Is it possible to develop model theory for models of $PA$, inside $PA$ itself (augmented with consistency raising assumptions such as $Con(ZFC)$ if necessary, but still in the language of $PA$)? What ...
0
votes
1answer
44 views

Bourbaki Proof in First Consequences? Use of Not?

In Bourbaki Theory of Sets English (c) 1970 Section 3.2 C6 there is a first consequence that I have questions about. I have attached images of the text here. My question is: We are told that A, B, ...
2
votes
1answer
66 views

Problem with a proof ( sequent calculus)

I have to proof this sequent: ⊢ (p → q) → ((q → r) → ((p v q) → r))) i ve already done sth like this ...
2
votes
0answers
36 views

What is the proof-theoretic ordinal of $ \mathsf{PA}+\mathsf{TI}(\prec_{\varepsilon_0})$?

$ \mathsf{TI}(\prec_{\varepsilon_0}) $ is transfinite induction on $\varepsilon_0$ ordinal notation by Cantor normal form. I think that proof-theoretic ordinal of $\mathsf{PA}+\mathsf{TI}(\prec_{\...
1
vote
1answer
66 views

Using structural induction to show derivablity

To prove a judgement is derivable by induction on it's derivation tree seems circular to me. From what I understand, structural induction works by proving a property $P$ for the base case of the tree (...
1
vote
1answer
67 views

Concise introduction to first-order deductive system with free-variable formulas

In first-order logic, sentences are a subset of (well-formed) formulas, viz. those that do not have free variables. With most deductive systems in the literature, one may only prove sentences, but not ...
0
votes
1answer
85 views

Confusion about soundness of sequent calculus

I'm currently reading a pdf textbook called Sets, Logic, Computation An Open Introduction to Metalogic Remixed by Richard Zach, and it covers sequent calculus LK and (partially) proves its soundness. ...

1
2 3 4 5
17