Tagged Questions

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

265 views

What are those “things that cannot be proved using only ordinary rules of inference”?

The online edition of the book Introduction to Logic by Michael Genesereth and Eric Kao, has a detail that left me confused. CHAPTER 4 [...] 4.2 Linear Proofs [...] The ...
26 views

Set-Theoretic Probability

Consider $\{B_i | i \in I\}$ be a collection of events where $I$ is an arbitrary index set. I would like to show that $$\left(\bigcup_{i \in I} B_i\right)^c = \bigcap_{i \in I} B_i^c.$$ My friend ...
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: ...
219 views

What is the proof-theoretic ordinal of the first-order theory of real closed fields?

I recently asked a question on MathOverflow, concerning a predicative second-order theory of real numbers. Now the standard way of developing predicativity in the case of second-order arithmetic is ...
165 views

Curry-Howard Correspondence (Proof Theory)

As you all know, the Curry-Howard correspondance provides a link between type theory and predicate logic. Concepts featured in the former, such as $\Pi$-type and $\Sigma$-type can, by the ...
53 views

What is the intutition behind the negative exponential ? in linear logic?

The positive exponential ! has a very satisfying interpretation in terms of the standard resource interpretation of linear logic. Given a resource $a$, we know that $!a$ means an infinite supply of $a$...
50 views

What is the proof-theoretic ordinal of $PA+TI(\epsilon_0)$?

what is the proof-theoretic ordinal for $PA+TI(\epsilon_0)$, where $PA+TI(\epsilon_0)$ is Peano arithmetic where transfinite induction up to $\epsilon_0$ was added? Is it known? Thank you
72 views

Infinitely many proofs?

While compiling a list of my favorite proofs of the infinitude of primes, the following came to mind; Proposition: There are infinitely many non-isomorphic proofs of the infinitude of primes. I'm ...
50 views

Inversion lemma for G3ip

I'm following the book Structural Proof Theory by Negri and others. In it, they claim on page 32 about G3ip that if $⊢ _ n A \& B, Γ ⇒ C$, then $⊢ _ n A, B, Γ ⇒ C$. But, given that the only ...
240 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 $\omega_1$-...
99 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 ...
69 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" ...
480 views

Difference between soundness and correctness

Is there any actual semantic difference between soundness and correctness? Can I use these words interchangeably when talking about formal reasoning, proof, logics, etc.? Otherwise, is there a ...
27 views

What to call a term-in-context whose context contains exactly the variables occurring in the term?

In type theory, a term-in-context $\Gamma \vdash t : \tau$ is only well-formed when $\Gamma$ contains all the variables occurring in $t:\tau$. Is there a name for when it contains exactly the ...
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: "...
80 views

Is the following derivation of Gödel's Paradox generalizable to an intuitionistic one using provability?

I will follow Goedel's original proof of Goedel's paradox located on pg. 264 of Hao Wang's A Logical Journey: From Gödel to Philosophy. With this in sight, and to also avoid confusion, I will also ...
90 views

34 views

Is the full strength of first-order logic needed for dealing with equational theories?

More specifically, if we have an equational theory $T$ (a set of equations understood as being implicitly universally quantified), are the (equational) consequences of $T$ that can be proved with ...
24 views

Independence of FLT over weak systems

It is known that Fermat's last theorem can be proven in finite-order arithmetic (e.g. accoridng to this site). This is still an extremely high upper bound on proof complexity (for example, compared to ...
65 views

Is a sentence in $\Pi_1$ true given $Q \vdash \lnot\varphi$?

If $Q \vdash \lnot\varphi$ (Q is the Robinson arithmetic), and if I assume that $\varphi \in \Pi_1$; Can I say that $\varphi$ is a true sentence? My thoughts are that, given that Q is $\Sigma_1$- ...
112 views

Do we know that if $\pi$ is normal then there is a proof of it?

We do not know whether $\pi$ is normal or it is not and many other weaker statements, e.g. (*) $\pi$ contains infinitely many $0$s. Inspired by the Godel's incompleteness theorem that there are some ...
47 views

A question about $KP + V = L$ and $KP$ set theory.

In reading Rathjen (Choice principles in constructive set theories) and Jager (On Feferman's OST) I've come across two facts that are taken as obvious/well known, and probably are, but for which I ...
65 views

Proof of $(\forall x. \varepsilon(x)) \Rightarrow \bot$ in $\lambda\pi$ calculus $\equiv$

What is the right representation of the proof of $(\forall x. \varepsilon(x)) \Rightarrow \bot$ in simple type theory as a term of $\lambda\pi$ calculus $\equiv$? Note on notation: The epsilon ...
92 views

proof checking machine vs. provability checking machine

Let M be a proof-checking Turing machine which takes two inputs, A and B. : M(A,B) = 0 if A codes a valid proof of the sentence coded by B in ZFC. M(A,B) = 1 if A does not code a valid proof of the ...
84 views

Examining every mathematical result in purely formal, ZFC language.

My main interest is physics. However, being self-taught in mathematics for the most part, my proofs tend to be more intuitive than it is acceptable. Yet, I recognize my inaptitude in rigor, and I ...