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

learn more… | top users | synonyms

0
votes
1answer
30 views

Gentzen-style proof system with global states?

I'm sorry if my question looks stupid or does not make sense. However, I want to ask if it is normal/common to have a global state, which is shared by all inference rules, in a Gentzen-style proof ...
0
votes
0answers
50 views

Is there a standard notation for coding finite sets of numbers as numbers?

Hajek and Pudlak Metamathematics of First-Order Arithmetic use the Ackermann encoding of hereditarily finite sets, but they use no notation for codes. They let the reader see from context when a ...
0
votes
0answers
11 views

Proving weak simulation

I want to prove something but I am not sure if it is the right way to do it. I have two LTS that define different semantics. A=($Q_a,Λ,\to)$, and B=$(Q_b,Λ\cup\{\beta\},\leadsto)$, where $\beta$ is ...
38
votes
3answers
4k views

Can proof by contradiction 'fail'?

I am familiar with the mechanism of proof by contradiction: we want to prove $P$, so we assume $¬P$ and prove that this is false; hence $P$ must be true. I have the following devil's advocate ...
1
vote
1answer
52 views

HPC: Prove that $\vdash A\to \lnot\lnot A$

Prove that $\vdash A\to \lnot\lnot A$ By Deduction Rule we know that it is sufficient to show that ${A}\vdash \lnot\lnot A$ I am also familiar with the formula: $\lnot A \vdash (A\to B)$. So if I ...
0
votes
0answers
49 views

Prereqisites for: Subsystems of second order arithmetic

As the title suggests, im wondering what the prerequisites for Simpsons book, Subsystems of... are? Unfortunately I cant find it in the preface. My background is a Bachelor in Philosophy and ...
2
votes
1answer
102 views

Can we prove that induction is impossible for some proofs?

I read in a book that Andrew Wiles first attempted proof by induction to prove Fermat's last theorem and that he gave up proving it with induction. Instead as far as I understand, Wiles proved some ...
4
votes
2answers
79 views

Why is it so hard to translate some proves into machine-readable form?

I have just read a topic on mathoverflow about man vs. machine in mathematics. The topic was inspired by the recent victory of Alpha Go over the World Go Champion, Lee Sedol. It reminded me of an ...
1
vote
1answer
18 views

Cannot create algorithm for decidable language

L2 = {<M> : M is a TM and there exists an input string w such that M halts within 10 steps on input w} Hi. I am creating an algorithm to show above L2 is ...
0
votes
0answers
37 views

Algebraic embeddings and isomorphisms in formalized ZFC

Example: It is always said that we can embed $\mathbb{Z}$ within $\mathbb{Q}$ by identifying $z \in \mathbb{Z}$ as $(z,1) \in \mathbb{Q}$. This is because there is an injective ring homomorphism $\phi ...
2
votes
0answers
48 views

Do we sometimes prove things based on the assumption that mathematics is self-consistent?

Do we sometimes prove things based on the assumption that mathematics is self-consistent? I recently started to be dubious about proofs by contradiction. It seems to me that it is somehow based on ...
1
vote
0answers
30 views

Equivalence between sequent calculi with different cut rules

Let G4' be a sequent calculus G4 for classical logic with the addition of the following pair of "left" and "right" cut rules: Let now be G4'' a second calculus G4 for classical logic with the ...
1
vote
1answer
35 views

Is $\neg \neg \forall \neg \neg A \leftrightarrow \forall \neg \neg A$ intuitionistic derviable?

Is the following a rule which is derivable in intuitionistic logic: $\neg \neg \forall \neg \neg A \leftrightarrow \forall \neg \neg A$ I thought that I read it somewhere,... hope that someone can ...
41
votes
12answers
6k views

Are proofs by contradiction really logical?

Let's say that I prove statement $A$ by showing that the negation of $A$ leads to a contradiction. My question is this: How does one go from "so there's a contradiction if we don't have $A$" to ...
1
vote
1answer
54 views

How is the non-existence of a solution proven?

I've been wondering how an argument that a solution to a particular problem doesn't exist is put together. For instance "Pour-El and Richards found an ordinary differential equation $\phi'(t)=F(t,\...
1
vote
0answers
83 views

Incompleteness theorems in encoding schemes other than Gödel numbering

Gödel's proof of his incompleteness theorems makes use of Gödel numbering, which is a device that allows a theory of arithmetic $S$ (e.g. PRA) to express and reason about metamathematical statements ...
3
votes
1answer
67 views

Is there a consistent arithmetically definable extension of PA that proves its own consistency?

Gödel's second incompleteness applies, for instance, to r.e. extensions of PA. I am wondering if it applies more generally to arithmetically definable extensions of PA. I see that there is a complete ...
0
votes
1answer
70 views

Is it possible to create a software to find formal proofs?

Let's say I have a Hilbert style system, with a few axioms and rules of inference, and I want to find a proof for some formula $\varphi$, is it possible to create an algorithm that would find a proof ...
45
votes
6answers
3k views

Proving the existence of a proof without actually giving a proof

In some areas of mathematics it is everyday practice to prove the existence of things by entirely non-constructive arguments that say nothing about the object in question other than it exists, e.g. ...
0
votes
1answer
36 views

Prove in GL that no statement can be proven consistent with PA unless PA is inconsistent

I'm trying to do a exersie on page 16 of this paper. It says: Exercise. Show, using the rules of Godel-Lob modal logic (GL), that $\square⊥ ↔ \square \diamond p$; recall that $\diamond p = ¬\...
3
votes
2answers
101 views

Can a mathematical theorem be proved in infinite ways?

This is a question that I really think about. I wanted to develop my mind, and started trying to prove the Pythagorean theorem of a triangle, trying each day, and now its been a week. I wonder if ...
1
vote
1answer
62 views

Is there a connection between local soundness and completeness in proof theory, and free objects in category theory?

I was watching Frank Pfenning's lecture series on proof theory, where he described the notions of local soundness, and local completeness. He described local soundness of a logical connective as, ...
2
votes
0answers
54 views

Does it make sense to claim that something cannot be proven without induction? [duplicate]

Often we have questions on this site which ask for a proof of some result without induction.1 It seems that when such a question is posted, it is quite well-understood what is meant by proof avoiding ...
1
vote
1answer
41 views

Can we assign a number to each theorem stating its complexity?

I was wondering if inside an axiomatic theory it could be possible to assign each theorem a number that indicates its complexity. Theorems with small complexity numbers would be "almost axioms"; if ...
5
votes
2answers
435 views

Programming and ZFC

Suppose I have a simple program that implements an algorithm (say depth-first search), written in a simple imperative programming language with the standard for loops, recursions, conditional ...
5
votes
5answers
197 views

what is a valid mathematical proof?

from what i have seen in my experience with math we can say that a valid proof is one that uses some form of logic (usually predicate logic) and uses logical rules of deduction and axioms or ...
0
votes
1answer
39 views

Must non-constructive existential proofs use axioms of foundation or choice?

I have been getting confused thinking about non-constructive proofs. Several axioms of ZFC imply existence of a set with certain properties, and for each axiom except foundation, infinity, and ...
0
votes
1answer
181 views

Can you prove that something is provable/unprovable? Give an example [closed]

Also, can something be unprovable by definition?
2
votes
2answers
112 views

A philosophical question about an hypothetical theorem/equation of everything

Preamble I'm not a mathematician. I'm just curious. Please forgive my pseudo formalism. Please allow me, a non mathematician, to have just questions. Definition A mathematical theorem is a statement ...
3
votes
2answers
115 views

Proofs about theorem-provers in ZFC, in ZFC

Is the following statement provable in ZFC for some $A$: "$A$ is an algorithm which, when given as input a proposition $p$ in the language of ZFC, outputs 'yes' only if $p$ is provable in ZFC, 'no' ...
0
votes
1answer
55 views

Equivalence rule for sequent calculus

Why are there no inference rules for equivalence (≡ on the right and ≡ on the left) for the sequent calculus, and if there was, how would they look like? e.g. (1) $\cfrac{?}{\Gamma,(A \supset B) ≡ (...
2
votes
1answer
124 views

Example of a probability theorem that requires axioms in addition to Kolmorogov's?

Probability theory, in it's more general form, is axiomatized by Kolmorogov's axioms: Kolmorogov's Probability Axioms Let $(\Omega,\mathcal{F},P)$ be a measure space. The three axioms are: ...
0
votes
1answer
54 views

Is there some result that says a theory cannot prove the consistency of any of its extensions?

Is there some result that says a (sufficiently strong) theory cannot prove the consistency of any of its extensions? Or something along these lines?? More generally, is there a result that says a (...
0
votes
2answers
89 views

Induction is the only way? [closed]

Are there any statements that are true and can only be proved by induction? (In most of the proofs I saw the induction proof shed some light on another way of proving a statement e.g. with ...
35
votes
11answers
3k views

What is exactly the difference between a definition and an axiom?

I am wondering what the difference between a definition and an axiom. Isn't an axiom something what we define to be true? For example, one of the axioms of Peano Arithmetic states that $\forall n:0\...
3
votes
0answers
53 views

Can every mathematical proof be seen as the verification of some algorithm's action?

Put another way: Can every mathematical proof be reformulated to be about some class of Turing Machines? Example Any proof of the existence of infinite prime numbers is equivalent to the statement: "...
2
votes
2answers
61 views

Number of proofs for a statement

On this site, people ask questions and then answers and proofs for those answers come from readers. Readers mark the best answer and then people focus on the next interesting topic. Sometimes, a ...
2
votes
1answer
62 views

Examples of theories with enough constants

A theory $\Gamma$ of $L$-sentences has enough constants if for every $L$-formula $\phi(x)$ with one free variable $x$, there is a constant $c$ such that $$\Gamma \vdash \exists x \phi(x) \rightarrow \...
2
votes
2answers
101 views

How does the Soundness Theorem follow from this lemma?

The soundness theorem is a famous theorem in logic that goes like this: If $\Gamma \vdash \phi$, then $\Gamma \vDash \phi$. It's supposed to follow readily from Lemma 3.2.3 from Moerdijk/Van ...
2
votes
2answers
250 views

Proof of completeness and soundness of a proof system

As stated here, https://en.wikipedia.org/wiki/List_of_rules_of_inference, "a set of rules can be used to infer any valid conclusion if it is complete, while never inferring an invalid conclusion, if ...
0
votes
2answers
74 views

Decidability of certain first-order statements

Is it possible to construct an algorithm that can formally prove any statement in some countable first-order theory except for exactly those which aren't provable in the theory? Why or why not? Edit: ...
2
votes
0answers
33 views

Disequality in Type Theory [duplicate]

Is it possible to prove $0 \neq 1$ in (non-univalent) Martin-Löf type theory, where $0$ and $1$ are natural numbers (defined using the usual inductive type $0 : \mathbb{N}$, $S : \mathbb{N} \to \...
1
vote
2answers
66 views

Inconsistent theory with uniformly long refutation?

I understand that there are theorems in PA that necessarily require "very long" proofs; cmp. [1]. On the other hand it seems interesting to think about Life in an inconsistent world. So is it ...
7
votes
3answers
342 views

Why can't you prove the law of the excluded middle in intuitionistic logic (for layman)?

I am learning about the difference between booleans and classical logics in Coq, and why logical propositions are sort of a superset of booleans: Why are logical connectives and booleans separate in ...
2
votes
1answer
102 views

Why does the dependent product type need “forall”?

I feel stupid asking this question because it is so fundamental to logic and math. However, in my starting to learn proof theory and now type theory, I have not seen an explanation on why you need the ...
5
votes
1answer
130 views

Completeness for Infinitary Logic?

I have heard a rumor that there is a proof system for certain infinitary logics, given by Carol Karp (?) in her thesis, but I can't find a copy. The result that I'm told exists is the following: A ...
5
votes
2answers
113 views

Is it possible to nonconstructively prove that a statement can be proven or disproven within a formal system?

I've heard of many examples of statements that have been proven to be independent of a formal system, meaning that they can't be proven within that formal system (for example, the Continuum Hypothesis ...
7
votes
1answer
174 views

WLOG and “by symmetry” arguments and the foundations of mathematics

John Harrison's paper Without Loss of Generality raises the interesting point that although "without loss of generality"/"by symmetry" arguments are a common proof technique, there is no corresponding ...
-1
votes
2answers
161 views

Can all theorems be deduced directly from the ZFC axioms?

I stumbled upon a website called metamath that claims to be able to do this : http://us.metamath.org/mpegif/mmset.html
0
votes
0answers
53 views

Proof of cut elimination

I am reading Proofs and types and am blocked at the proof of cut elimination in sequent calculus (chap 13). I don't see either how the cuts are being pushed up above the preceding steps to the top of ...