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

1
vote
0answers
79 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
65 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
35 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
97 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
59 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
429 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
194 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
158 views

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

Also, can something be unprovable by definition?
2
votes
2answers
110 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
114 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
123 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
53 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
88 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 ...
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
1answer
46 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
98 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
223 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
73 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
330 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
89 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
123 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
167 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
155 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 ...
4
votes
0answers
61 views

Proof by reflection and Homotopy Type Theory

I have been looking into various proof assistants, and came across the method of proof by reflection in Coq, which (from what I understand) allows one to verify a program provides the correct "answer" ...
6
votes
3answers
697 views

What does “rigorous proof” mean?

I have heard several times that some mathematician has given another and more rigorous for an established theorem, but I don't know what does it really mean and what differences makes it to be more ...
0
votes
1answer
35 views

Problem with a step in a proof in predictive control

I'm trying to follow a demontration written in an optimal control paper. In one of the steps, it states What I'm having troubles with is the last step, it states that because of the convexity of ...
6
votes
0answers
81 views

What are some arguments/counterarguments for Zeilberger's “proof certificates”?

Here is the quote I wish to ask about: "I speculate that similar developments will occur elsewhere in mathematics, and will 'trivialize' large parts of mathematics, by reducing mathematical ...
2
votes
1answer
76 views

Encyclopedia of Mathematical Proofs with no English

I was wondering if anyone is aware of a modern book that builds a subset of elementary number theory from Peano axioms preferably in a Principia Mathematica fashion? Or similarly an encyclopedia of ...
3
votes
1answer
114 views

Consistent, complete axiom system that proves its own consistency

Is there a consistent, complete axiom system that proves its own consistency? I know that this question isn't exact and I haven't defined when an axiom system proves its own consistency because ...
0
votes
1answer
85 views

What kind of trivial statement still needs to be proven?

There are many statements that seem to be needless of a proof since they are ‘evident’ mainly because of our intuition. But some of them have proofs. For example, in C. Adams’ Introduction to ...
10
votes
0answers
233 views

The ethics of Borel determinacy

I was speaking with a friend the other day, and I happened to say "morally, Borel determinacy is as strong as ZF." I was riffing on the well-known result of Harvey Friedman, that we need ...
1
vote
0answers
55 views

Show that if A and B are strictly convex, then A + B is strictly convex or provide a counter example.

We have: If A is open: $\exists x,y \in A,$ $x \neq y$ such that $\lambda x+(1-\lambda y)\in \dot A $ (the interior) and $\exists u,v \in B,$ $x \neq y$ such that $\lambda u+(1-\lambda v)\in ...
4
votes
8answers
238 views

Why is $n^2+4$ never divisible by $3$? [duplicate]

Can somebody please explain why $n^2+4$ is never divisible by $3$? I know there is an example with $n^2+1$, however a $4$ can be broken down to $3+1$, and factor out a three, which would be divisible ...
9
votes
3answers
136 views

role of definitions in proofs

Definitions are needed to define objects and such, however I am confused as to where definitions come from. I feel that they cannot be something that we arbitrarily define because simply saying ...
35
votes
2answers
437 views

When are two proofs “the same”?

Often, we find different proofs for certain theorems that, on the surface, seem to be very different but actually use the same fundamental ideas. For example, the topological proof of the infinitude ...
1
vote
2answers
155 views

How can I start to learn proof theory?

I'm studying computer science and I realized that I have problems in working with mathematical proofs. They are for example part of my class Formal Systems and Automata. I'm really interested in ...
0
votes
0answers
70 views

A provability puzzle

This is a problem I came up with on my own, and it has me stumped, so I am going to pose it as a kind of puzzle. Let $F$ be a formal proof system, recursively axiomatizable, with an acceptable ...
1
vote
1answer
105 views

What does it mean by Proving false

With respect to the recent finding of a bug in a Coq theorem prover in which false was proved, I'm asking this question. As a hobbyist studying maths, I'm ...