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-* ...
710 questions
1
vote
1answer
24 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
27 views
theory scope and proof [on hold]
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
52 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
26 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/...
0
votes
0answers
98 views
+50
Alpha Test ZoomSpace - A futuristic mathematician's tool.
Remark. This version only has diagram editing capabilities, and plenty of bugs for you to report.
Future versions, maybe in about 2 months, will have basic diagram chasing features.
ZoomSpace v0.0 (...
1
vote
0answers
24 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
81 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 ...
0
votes
0answers
38 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
60 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))$, ...
0
votes
0answers
34 views
Questions in proof theory (PRA-provability of EA-theorems, Girards book from '87)
I am working through the above mentioned book, 'proof theory and logical complexity, volume 1', with some trouble here and there.
I would be glad if someone can help me with some of the exercises, ...
0
votes
0answers
19 views
Questions in proof theory (interpretation of PRA in PA, Girards book from '87)
I am working through the above mentioned book, 'proof theory and logical complexity, volume 1', with some trouble here and there.
I would be glad if someone can help me with some of the exercises, ...
1
vote
1answer
56 views
Questions in proof theory (Definition of an interpretation of one theory in another, Girards Book from '87)
I am working through the above mentioned book, 'proof theory and logical complexity, volume 1', with some trouble here and there.
I would be glad if someone can help me with some of the exercises, ...
1
vote
0answers
53 views
Questions in proof theory (PRA-provability of an EA-axiom, Girards Book from '87)
I am working through the above mentioned book, 'proof theory and logical complexity, volume 1', with some trouble here and there.
I would be glad if someone can help me with some of the exercises, ...
1
vote
2answers
83 views
Prove $f_n \to f$ uniformly on $\mathbb{R}$
Denote by $D$ the set of all continuous, increasing functions $f: \mathbb{R} \to [0, \infty)$ such that $\lim \limits_{x \to - \infty} f(x) = 0 $ and $\lim \limits_{x \to + \infty} f(x) = 1 $. If $f_n,...
2
votes
3answers
66 views
Show that $\Sigma \vdash\varphi$ if and only if $\Sigma\,\cup \{\neg\varphi\}$ is inconsistent.
I am stuck at the following problem:
Let $\varphi$ be a sentence in a predicate calculus $T$ and $\Sigma$ a set of sentences in $T$. Show that $\Sigma \vdash\varphi$ if and only if $\Sigma\,\cup \{\...
0
votes
1answer
36 views
Proving a statement of the form $P\rightarrow(\lnot Q\lor \lnot R)$.
Not looking for a proof of my question, only an answer to my question below.
Question: I want to assume that $P$ is true for this proof, then if I assume that $Q$ is also true and conclude that $R$ ...
0
votes
1answer
57 views
show that for every consistent theory there is a complete consistent theory
Let $\mathcal{L}$ be any language of predicate logic, $\Sigma_0$ a consistent theory in $\mathcal{L}$. Let P be the set of all consistent theories $\Sigma \supseteq \Sigma_0$ in $\mathcal{L}$.
With ...
2
votes
1answer
82 views
proof of formula with Peano-axioms
For all natural numbers n define $\Delta_n$ as:
$\Delta_0$ is the constant $0$ and $\Delta_{n+1}$ is $S(\Delta_n)$.
Here is S the function for the follower, i.e. $\forall x: S(x) = x+1$.
1)I want ...
-1
votes
0answers
39 views
A false statement that can't be disproved without using a counterexample
When one wants to disprove a statement, finding a counterexample is easier than 'proving a statement is false' in most cases(I don't know if I'm using the right expression here, but I hope you know ...
1
vote
1answer
85 views
The use and meaning of the “tilde-equal-symbol” for partial (recursive) functions in Girards monograph 'proof theory and logical complexity, volume 1'
English is not my native language, so please forgive if I do not express myself properly.
I am working with the book named above on proof theory, and I have a little problem with the authors use of ...
11
votes
6answers
1k views
Does a mathematical proof in $\mathbb{C}$ imply a proof in the $\mathbb{R}$? [closed]
Does every proof in the complex numbers also prove the statement in the real numbers? I thought it might be true, because the real numbers are part of the complex numbers.
0
votes
0answers
27 views
Are there any statements $\phi$ where “$\vdash \phi$ or $\vdash \neg \phi$” was shown nonconstructively?
I am wondering if there is an example of a statement $\phi$ in the language of some formal system $T$ satisfying (1-4):
$\phi$ was shown to not be independent of $T$ (i.e. it was proved that $T \...
2
votes
1answer
96 views
When does $(\square P \land \square Q) \to \square (P \land Q)$ hold?
If all axioms of classical propositional calculus hold and we work in modal logic that is at least K (ie. extremely weak), it is trivial to show $\square(P \land Q) \to (\square P \land \square Q)$. ...
0
votes
1answer
27 views
Theorem statable in base system but not provable in base system?
On the wikipedia page for proof theory, under the section of reverse mathematics, it is stated that:
For each theorem that can be stated in the base system but is not provable in the base system, ...
3
votes
0answers
61 views
Formal proof of $\exists x (\exists y P(y) \rightarrow P(x))$ and $(\forall x \exists y R(x,y))\rightarrow (\forall y \exists x R(y,x))$
within the following axiomatic system I've beeb trying to proof the formulas
(1) $\forall x \exists y R(x,y) \rightarrow \forall y \exists x R(y,x) \\$ and (2) $\\ \exists x (\exists y P(y) \...
8
votes
1answer
85 views
A theory which seems to have proof-theoretic ordinal $\omega_1^{CK}$
I'm trying to understand proof-theoretic ordinals, and mistakenly "proved" there's a sound recursive theory of arithmetic with proof-theoretic ordinal $\omega_1^{CK}.$ That's impossible, so where does ...
1
vote
1answer
36 views
For all positive integers $a, b$, if $a$ is composite and $a$ divides $b$, then $b$ is composite.
this question is in my practice midterm and it does not have solutions, I want to make sure my proof is correct.
Proof:
suppose integers a and b, and suppose a is composite therefore we can write a ...
3
votes
2answers
72 views
Are all “Theorems” necessarily in the “if - then” form?
When someone talks about "Theorems" in Mathematics, something of the sort below comes to my mind.
Theorem 1: For every two real numbers $a$ and $b$ with $a \lt b$, there
exists a rational number $...
-1
votes
1answer
61 views
Help with natural deduction system (Propositional logic) [closed]
In natural deduction, I'm trying to get to $(A \to B) \land (\lnot A \to C)$ from the following formula:
$(A \land B) \lor (\lnot A \land C)$
and vice-versa, i.e.
$(A \land B) \lor (¬ A \land C) \...
3
votes
0answers
48 views
Model for the type-theoretic axiom of choice in Coq.
This is the request for references.
It is a known fact that there is a model of ZFC in ZF, so ZFC is consistent if ZF is consistent.
It is also know that there is a double-negation Godel-Gentzen ...
0
votes
2answers
42 views
Proof by strong induction
$F(0) = 0$
$F(1) = 0$
$F(n) = 1 + F(n-2)$ , when $n > 1$
Prove by strong induction that $F(n)=n$ div $2$ for $n\geq0$
$a$ div $b$ is a integer division. So $10$ div $2 = 5$, $11$ div $2 = 5$, $...
5
votes
0answers
43 views
How much arithmetic is required to formalize quantifier elimination in Presburger arithmetic?
As we know, Presburger arithmetic can be proved decidable by demonstrating that it admits quantifier elimination, i.e. that there is an algorithm that reduces any sentence in the language to some ...
0
votes
5answers
70 views
Starting with a false statement, how can one prove anything is true? [duplicate]
So I've been learning a bit of logic for class and heard that if you begin with a false statement, you can then prove anything to be true, however I don't entirely understand what this means or how to ...
2
votes
1answer
65 views
Proving that $\{P_1,P_2, \dots, P_n\}$ is complete but not maximally consistent
Prove that $\{P_0,P_1, \dots, P_n\}$ is complete but not maximally consistent
So I need to prove that this is complete, consistent, but not maximally consistent. But I have a few confusions about ...
1
vote
1answer
39 views
$\Sigma ; \lnot \alpha \vdash k $. Prove that $\Sigma \vdash \alpha$
$k$ is a contradiction such that it belongs to a set of well-formed formulas. $\Sigma ; \lnot \alpha \vdash k $. Prove that $\Sigma \vdash \alpha$ where $\alpha$ is a well-formed formula.
After ...
0
votes
1answer
25 views
Reasoning behind proof by contradiction
I am aiming to understand the style of argument that mathematical logic is a form of, so in some ways my question might seem more philosophical than mathematical but please bear with me.
So, ...
1
vote
1answer
27 views
Is there a category of logical propositions and deductions? [duplicate]
I'm looking for a rigorous definition of the category defined (by handwaving) as such:
objects are "logical propositions" (first order formulas?),
morphisms are "logical deductions" between them (...
0
votes
2answers
27 views
Impossibility of a short formal proof of a famous problem
Is it possible to prove by enumeration or other means that there cannot be a formal proof shorter than given length of a famous conjecture?
In particular, is it easy, given a formal proof of a ...
0
votes
2answers
55 views
Prove Logic Using Proof of Contradiction
Prove the following using proof of contradiction:
a → c
b → d
(c ∨ d) → ¬e
(e ∨ f) → (a ∨ b)
∴ ¬e
What I have done so far is:
...
0
votes
2answers
38 views
Prove Logic Using Hypothetical Reasoning
Prove the following using hypothetical reasoning.
¬(a ∧ ¬b)
¬(b ∧ d)
∴ (d → ¬a)
What I have done so far is:
...
0
votes
2answers
26 views
Proving Symbolic Logic
Prove that the following is valid:
b ∧ a
a → c
(c ∧ ¬d) → ¬b
∴ d
So far I have only done:
b (Rule of Conjunctive Simplification on b ∧ a)
b ∨ (c ∧ ¬d) (Rule of Disjunctive Amplification on b)
...
0
votes
2answers
23 views
Symbolic Logic Proof?
I was given the following argument:
If there is a, there is b and if there b there is c. Thus there is a but no c.
Which I put into symbolic form:
(a $\rightarrow$ b) $\land$ (b $\rightarrow$ c)
$...
0
votes
1answer
45 views
Need help for a proof ( sequent calculus )
I have to prove the following:
$$\vdash((A \to B) \land (B \to A)) \to (A \leftrightarrow B)$$
But I'm totally stuck here after using introduction of implication and introduction of equivalence:
\...
0
votes
3answers
47 views
Is this a correct mathematical statement about integers mod n and congruence mod n? [closed]
Let's say we have the congruence: $b \equiv a \mod 20$
Is it then correct to say that $(b \equiv a \mod 20 )= \mathbb{Z}_{20}$
where $\mathbb{Z}_{20}$ is the set of residue classes or set of ...
0
votes
1answer
37 views
Can a sequent be valid if the conclusion contains atoms that are not in the premise?
Is it possible to prove the validity of the following sequent:
$p \vdash (p \to q) \to q$
Here, our premise is that $p$ is True. The conclusion references a new atom, $q$.
I would argue that this ...
4
votes
1answer
75 views
Do there exist true statements with only one proof? [closed]
The Pythagorean Theorem, for instance, has many, many proofs which are fundamentally different and use what appear to be very different ideas. These range from static geometric constructions to ...
3
votes
1answer
76 views
Can meta-languages disagree over what an object language proves?
Suppose we have a language/theory $\mathcal{L}$ in First Order Logic, and we look at what it proves. Is it possible that there are two meta-languages/theories, say $\mathcal{L_1}$ and $\mathcal{L_2}$, ...
2
votes
1answer
77 views
How can any proof of Gödel's incompleteness theorem be accepted considering systems of mathematics themselves are incomplete?
I believe there are at least several proofs of Gödel's incompleteness theorem. Nagel and Newman wrote a book (1958) that presents one in particular.
But considering the theorem itself exposes ...
0
votes
0answers
52 views
McNaughton functions and hypersequents for Lukasiewicz logic
For this question, all definitions are borrowed from Proof theory for fuzzy logics (2008) by Metcalfe, Olivetti, and Gabbay.
Consider a propositional language over $\{\rightarrow,\bot\}$ for infinite ...
5
votes
0answers
178 views
Is many sorted logic really a unifying logic?
I am reading "Extensions of First Order Logic" by Maria Manzano (1996). It develops the thesis that
"[M]ost reasonable logical systems can be naturally translated into many-sorted first order ...
