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.
6
votes
2answers
65 views
Can a mathematical proof always be objectively determined as correct or incorrect?
Fields medalist Michael Atiyah claimed a simple proof of the Riemann hypothesis, but many mathematicians rejected his proof. Am I right in saying that Atiyah's proof is either objectively correct (...
1
vote
1answer
69 views
Inversion lemma proof
I am following Structural Proof Theory by Negri and others, and I don't understand the Inversion Lemma proof (i) (the system is G3$_{ip}$, which is the same as G3$_i$ only that it excludes quantifier ...
2
votes
0answers
39 views
What will be the notion of a “valid deduction” in the following system?
Consider the Propositional Calculus whose axiom schemes and rule of inference are given below (here $P,Q$ and $S$ are formula schemes,
$\color{crimson}{\text{Axiom 1.}}\ P\to (Q\to P)$
$\...
3
votes
1answer
73 views
First orderer logic completeness and independence: the proof that disappear?
Gödel completeness theorem for the first-order logic is in fact equivalent to BPI (every proper filter can be extended to an ultrafilter). Moreover, BPI is independent of ZF; that in particular means ...
1
vote
1answer
44 views
Unprovable sentence, but provably it is provable.
Work in Peano Arithmetic, PA. Let Prov(n) be a standard proof predicate, so that $PA \vdash Prov(\ulcorner \phi \urcorner) \text{ iff } PA \vdash \phi$ .
By Löb's theorem, we know that if $PA \vdash ...
14
votes
2answers
816 views
Has a conjecture ever originally been decided by constructing the proof with mathematical logic?
So, one of the things that mathematical logic does is study theorems as abstract objects. There also many theorems about mathematical logic, and these theorems can have connections to other fields.
...
-2
votes
3answers
44 views
If $A$ is non-singular, is $-A$ non-singular? [on hold]
Prove or contradict:
If $A$ is invertible, then $-A$ is invertible as well.
-3
votes
2answers
27 views
Rational Numbers Proof
Apologies for the vagueness before, I'm new here. I hope this clears it up:
Show that, for all non zero $b\in \Bbb Z$, $${(0,b)}=((a',b')\in F:a'=0)$$ $$F=((a,b)\in \Bbb Z*\Bbb Z: b\ne 0))$$ where F ...
3
votes
2answers
25 views
Formal proof of distributivity of conjuction
I'm trying to prove that $\vdash p\land (q\lor r)\to(p\land q)\lor (p\land r)$ in natural deduction.
...
0
votes
1answer
36 views
Provide sequent calculus proofs of the axioms of the $\{→,∀,⊥\}$-fragment of the Hilbert system $H_c$
Could anyone please help me to understand what the question is asking?
Theorem: G1$_i$ + Cut $\vdash \Gamma \Rightarrow A$ iff H$_i$ $\vdash \Gamma \Rightarrow A$
1) Prove equivalence of G1$...
5
votes
0answers
51 views
Axiomatizing a “bounded” companion to PA
There's nothing special about PA here, I'm just focusing on it since it's strong enough to ignore lots of minor technical issues around foundations. If switching to some other theory would yield a ...
0
votes
1answer
25 views
Example of a $Δ_1$-formula that is not $Δ_0$ (arithmetical hierarchy).
In the arithmetical hierarchy, the class of $Δ_1$-formulas is defined as the intersection of $Σ_1$- and $Π_1$-formulas. It is obvious that every $Δ_0$-formula is $Δ_1$, but not every $Σ_1$- or every $...
0
votes
1answer
53 views
If Γ ⊢ A, then Γ ⊨ A
I'm having a difficult time differentiating between the two proofs:
1. If Γ ⊢ A, then Γ ⊨ A
vs.
2. If ⊢ A, then ⊨ A
Here's the question:
Prove “strong soundness”: for any set of formulas, Γ, and ...
0
votes
0answers
69 views
Can you recommend literature - easy/gentle/for self-study/introductory… - for the following topics…?
I am looking for literature that is as self-explanatory, easy, gentle, readable to the beginner, suitable for self-study, etc.. as possible, in the following fields.
(I mean the mathematical part as ...
1
vote
1answer
28 views
Regarding L$\to$ rule in sequent calculus and difference between G1$_c$ and G1$_i$ system
I am going through Troelstra and Schwictenberg's Basic Proof Theory, and I can understand most of the sequent calculus rules by finding some sort of parallel between the rule and a corresponding ...
0
votes
1answer
46 views
Swapping elements to form a specific permutation - Formal Proof
Considering a permutation of [1, 2, ..., n], it is fairly obvious that on doing n/2 swaps we arrive at the permutation [n, n-1, ..., 1].
This can be achieved by swapping the first element with the ...
2
votes
4answers
86 views
Proof of $(P\to Q) \vee (Q\to P)$ with natural deduction
I need to prove the following statement in natural deduction:
$$(P\rightarrow Q) \lor (Q\rightarrow P)$$
I tried assuming not (target statement) and assuming the left hand side, but I don't know ...
1
vote
4answers
65 views
Formal Deduction (logic) Question: $\lnot C, (B \to \lnot C) \to A \vdash (A \to C) \to F$
I've been stuck on this question for around two hours now.
I'm trying to prove that:
$\lnot C, \ (B \to \lnot C)\to A \vdash (A \to C)\to F $
I'm trying to get my second last step to be:
$\lnot C,...
1
vote
1answer
26 views
Proof equivalence relation with functions
We define 2 function: $f : X \rightarrow X$ and $g : X\rightarrow X$ and we define $ V(f,g) = \{x \in X | f(x) \neq g(x) \} $. Next we define a relation $R$ on the set Fun($X,X$) of all functions ...
0
votes
1answer
34 views
Proving certain obvious tautologies in the calculus of constructions
I'm trying to prove that $\lnot (\exists y : S.Py) \rightarrow \exists y : S. \lnot Py$ (let me know if the encoding of $\exists$ matters!). I don't have any good ideas about how to do that, but I've ...
1
vote
0answers
17 views
Classification of Proof Techniques
A few introductory papers and Wikipedia contain incomplete lists of proof techniques, e.g.:
direct
by induction
contraposition
contradiction
Are there classifications of proof techniques that ...
0
votes
1answer
41 views
How to prove the following formula using indirect proofs?
I have to prove the conclusion $(A \to B) \vee (B \to C)$ using nothing but formal proof rules for propositional logic (so introduction and elimination rules). Here's what I've done so far.
Proof
...
4
votes
0answers
83 views
Arithmetic systems without Induction
It's often said that AC is a controversial axiom and so often in my math classes when it is used a brief comment is made to the effect of "we can prove this without Zorn's Lemma but it's more work". ...
1
vote
0answers
17 views
Relation between strong normalization (say, of Godel's T) and consistency of a proof system (say PA)
I'm studying proof theory and type theory, mostly from "Lectures on the Curry-Howard Isomorphism" and Girard's "Proofs and Types" but some things aren't quite clear. In particular, with the regards to ...
2
votes
1answer
107 views
What is the purpose of Semantics/Model theory in Mathematical Foundations?
First off I know very little model theory so apologies if I say anything very dumb or offensive to logicians/model theorists. Second I should note that a lot of what I am saying here is motivated by ...
3
votes
2answers
71 views
How to use natural deduction to show $\neg (P \land Q) \vdash \neg P \lor \neg Q$?
How to use natural deduction to show $\lnot (P \land Q) \vdash \lnot P \lor \lnot Q$? I think I need to first assume $\neg(\neg P \lor \neg Q)$ and then find a contradiction but I cannot see how to do ...
0
votes
1answer
56 views
If statement A requires B to be true, is it possible to prove A without using B?
[it is totally described in the title in fact]
I have a statement A that is true only if statement B is true.
Is it possible to prove A without referring to B in any way? (I mean, if you use ...
2
votes
0answers
84 views
Is there a notion that quantify the dependence of a proof on AC?
The title is the question. I apologize if this is a naive question. I know there are weaker versions of AC, but this is not what I am looking for. For example, is there a theorem that its proof ...
-2
votes
1answer
37 views
Prove that $\sqrt{1+a} + \sqrt{1+b} + \sqrt{1+c} \leq 4$ [closed]
I am trying to prove this inequality but I am having some difficulties.
$\sqrt{1+a} + \sqrt{1+b} + \sqrt{1+c} \leq 4$
Edit: sorry i forgot to add a crucial info:
$a + b + c = 2 $ and $a,b,c \in R+$
1
vote
0answers
75 views
How do you determine if a geometric construction has degrees of freedom?
I would like to know if there is a common approach to proving or disproving whether degrees of freedom exist after following a geometric construction scheme? To clarify, that the result of the ...
0
votes
0answers
19 views
Formalization of an Intuitive Proof of the Surface Area of a Sphere
Consider the following proof that the surface area of a sphere is $4 \pi r^2$.
First let's try to squash an arbitrary sphere into its net. If we cut the sphere in half then open it up, we get two ...
1
vote
1answer
69 views
Proving A $\implies$ B or A $\implies$ C
To prove A $\implies$ B or A $\implies$ C with a direct proof, I'm confused on what we can assume. Normally for $A \implies B$ we assume A then prove B is true.
For proving A $\implies$ B or A $\...
-4
votes
1answer
103 views
Is this description of “ordinary induction” from Velleman's *How to Prove It* correct?
The following is from How to Prove It: A Structured Approach, 2nd edition, by Daniel J. Velleman, page 289.
To see why strong induction works, it might help if we first review briefly why
...
2
votes
0answers
50 views
Show that the proof rule is not sound and proof question
I'm asked to show that the proof rule
\begin{equation}
\dfrac{\varphi \to \psi}{\lnot \varphi \to \lnot \psi}
\end{equation}
is not sound.
To show this would I just make the truth tables for the ...
2
votes
1answer
46 views
When should I use RAA in natural deduction proofs?
I can't understand exactly when should I use RAA (reductio ad absurdum) rule in natural deduction proofs? What situation should "trigger" me to think "Now it's time to use RAA"?
1
vote
0answers
32 views
About provable-recursive functions in EA
Find $\forall$-axiomatisation of definitional extension of EA with functional symbols for all Kalmar elementary functions. Then use Herbrand's theorem to find the class of provable-recursive functions ...
0
votes
0answers
34 views
Validity of “rank” construction in Manin's proof of Lemma 6.7 for Gödel's completeness theorem
The question is about the proof of Lemma 6.7 in Yuri Manin's "A Course in Mathematical Logic", which is part of the proof of Gödel's completeness theorem.
Lemma 6.7 If $\mathcal{E}$ is consistent ...
0
votes
1answer
44 views
Question about Manin's proof of Fundamental Lemma 6.5 for Gödel's completeness theorem
In the course of the proof of Lemma 6.5 in Yuri Manin's "A Course in Mathematical Logic", the author states that a certain set of first-order logic formulas $\mathcal{E}$ is consistent, complete and ...
0
votes
1answer
35 views
Henkin conservative extension of an empty theory
Say we have the language $L = \{C, P\}$ where $C$ is a nullary predicate and $P$ a unary one. Then we consider the empty theory $E$ over the language $L$. My task was to give an example of a Henkin ...
2
votes
1answer
52 views
Conservative extension of an empty theory
Say we have the language $L = \{C, P\}$ where $C$ is a nullary predicate and $P$ a unary one. Then we consider the empty theory $E$ over the language $L$. What does a conservative extension of $E$ ...
2
votes
0answers
110 views
n-consistency - provability/truth of $\Sigma^0_n$ and $\Pi^0_{n+1}$ -formulas; n-consistent extensions, etc.
I am facing difficulties with the following exercise.
(It is 1.5.9. from 'proof theory and logical complexity', Girard, '87)
(i) T is $\textbf{n-consistent} \ (n>0)$ if any $\Sigma^0_n$ - theorem ...
0
votes
1answer
34 views
recursive inseparability of the two Gödelnumber-sets: theorems and 'anti-theorems' of EA
Here again one of my more or less basic proof-theoretic questions, working through Girards monograph from '87.
This is about exercise 1.5.10. - "recursive inseparability", on page 80.
It is this:
...
1
vote
1answer
40 views
proof by finding suitable instances and resolution
I am trying to proof by resolution the following:
1) Given a language with the binary relation symbols $<, <<, <<<$ and the binary function symbols $+, *$ and the constant symbols ...
0
votes
1answer
34 views
theory scope and proof [closed]
I am looking for the proposition which states that a theory rules scope cannot defined all versions of a proposition because it is kind of creating a circle.
Forgive my french.. And ...
2
votes
1answer
69 views
Ordering between formal theories by provability of consistency
I am studying proof theory with Girard's monograph from '87 ('proof theory and logical complexity').
1.5.6. is an exercise called 'ordering between theories'.
It reads as follows:
" (i) Let $\...
1
vote
0answers
43 views
Are the HBL derivability conditions necessary for Gödel's incompleteness theorems? (For Löb's theorem?)
I am currently working with 'proof theory and logical complexity', a monograph on proof theory.
In the exercises of the first chapter one was asked to prove Löb's theorem (https://en.wikipedia.org/...
1
vote
0answers
33 views
Is it possible to prove consistency of an axiomatic system without providing a model?
Providing concrete models is more-or-less impossible, since we are not sure about many things in real world. On the other side, abstract models are usually insufficient for proving consistency, since ...
1
vote
1answer
95 views
An alternative formulation (or corollary) of Tarski's theorem? [Or just a typo?]
In my proof theory monograph (proof theory and logical complexity, Girard from '87) there is an exercise 1.5.4. on page 78 called 'Tarski's theorem'.
It says:
"Show that there is no truth predicate ...
1
vote
0answers
108 views
Why the 'natural' consistency proof of PA cannot be carried out $\textbf{in}$ PA
In my proof theory monograph there is this exercise:
"The natural proof of PA cannot be carried out in PA. Why?
(This proof consists in showing that all theorems of PA are ture.)"
Apparently, by '...
0
votes
1answer
65 views
infinite and uncountable structures in specific classes of structures
I'd appreciate your help with proofing one or both of the following statements:
1) let $M$ be an infinite countable structure. We want to show that there's an uncountable structure in $Mod(Th(M))$, ...
