Stack Exchange Network

Stack Exchange network consists of 174 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

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-* ...

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