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.
818
questions
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. ...
