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

Filter by
Sorted by
Tagged with
3 votes
1 answer
73 views

Natural Deduction: An unusual(?) presentation

1. Context On page 241 of their paper Natural deduction and coherence for weakly distributive categories Blute et al give the right- and left-introduction rules of multiplicative conjunction for (...
user avatar
  • 1,707
2 votes
0 answers
60 views

Proofs and Types: Girard's remarks on Theoretical Computing

In the first chapter of Girard's Proofs and Types (1989) one finds the following remarks: Theoretical Computing is not yet a science. Many basic concepts have not been clarified, and current work in ...
user avatar
  • 1,707
25 votes
5 answers
2k views

Are there are any inherent mathematical reasons some proofs are difficult?

This is not a complaint about my proofs course being difficult, or how I can learn to prove things better, as all other questions of this flavour on Google seem to be. I am asking in a purely ...
user avatar
  • 466
1 vote
0 answers
83 views

Is consistency with the $\omega$-rule absolute to $\omega$-models?

According to Wikipedia, a theory $T$ that interprets arithmetic is consistent with the $\omega$-rule if and only if it has an $\omega$-model. That would mean that consistency with the $\omega$-rule is ...
user avatar
1 vote
1 answer
111 views

Why Hilbert's 24th Problem is unsolvable?

Hilbert's famous 24th problems handles the problem of the simplest possible proof of a mathematical statement, in a nutshell. It is said that there are a few problems with this problem. First of all, ...
user avatar
0 votes
0 answers
15 views

Conservativity and proof-theoretical ordinals

I assume the second-order arithmetical theory $T$ in concern is consistent and r.e. The most well-known kind of proof-theoretical ordinal $\|T\|$ of $T$ is the $\Pi_1^1$-ordinal, defined as $\|T\|=\{$...
user avatar
  • 11
1 vote
0 answers
21 views

Formulas that can be proved from the uniform reflection schema

Let $T$ be a sound, r.e. theory containing elementary arithmetic. By the uniform reflection schema of $T$ ($\mathrm{RFN}(T)$) I mean the schema that expresses the soundness of $T$: $\forall x(\...
user avatar
  • 11
1 vote
0 answers
17 views

Strength and conservativity of $\Sigma^1_n \textrm{-DC}_0$

How strong is $\Sigma^1_n \textrm{-DC}_0$ in terms of consistency strength? I know it is conservative to $\Pi^1_n \textrm{-TI}_0$, but I don't know its relation to other subsystems. Are there any ...
user avatar
  • 233
2 votes
0 answers
88 views

In the context of Morse–Kelley set theory how does truth compare to satisfaction in an unbounded class of $V_\kappa$s?

I've been studying Vopenka's principle: For any language $\mathcal{L}$ and a proper class $C$ of $\mathcal{L}$-structures, there exist distinct $M, N \in C$ and an elementary embedding $j: M \to N$. ...
user avatar
  • 233
2 votes
1 answer
138 views

Is there a distinction between rules of inference and axioms in Homotopy Type Theory (HoTT)?

I'm taking rules of inference to be metalinguistic and to describe when you can write down a certain syntactic expression in the object-language given that you already have others written down (e.g. &...
user avatar
0 votes
1 answer
47 views

Is it possible to use order relation in Presburger arithmetic?

The signature of Presburger arithmetic contains only the addition operation and equality, omitting the multiplication operation entirely. Is it possible to state and prove theorems in Presburger ...
user avatar
  • 387
1 vote
1 answer
41 views

Can Peano arithmetic be completed using only atomic $\omega$-completions?

Say we have an axiomatizable theory $T$ extending $Th(A_E)$ where $A_E$ are the axioms of arithmetic. What I call an atomic $\omega$-completion of $T$ (I am not sure if there is a more standard ...
user avatar
  • 58.7k
0 votes
0 answers
52 views

Are logical rules logics?

When I asked whether the empty logic (the one on which no argument is valid) is axiomatizable, the consensus was that it is, and that it is axiomatized by a proof system having no rules whatsoever. Is ...
user avatar
0 votes
1 answer
58 views

Prove that $\mathbf{L}$ is almost a normal modal logic.

Suppose we have a logic $\mathbf{L}$ containing all the propositional tautologies and the formula $\square(p\wedge q)\leftrightarrow(\square p \wedge\square q)$, and it is closed by Modus Ponens, ...
user avatar
  • 815
2 votes
0 answers
50 views

Is the empty logic axiomatizable?

Obviously this is a bit of an edge case. By the empty logic I mean the one on which all arguments are invalid, i.e. $\Gamma \nvdash \varphi$ for all sets of formulas (premises) $\Gamma$ and any ...
user avatar
3 votes
0 answers
193 views

Which sentences are irreducibly self-referential?

Below, all sentences/formulas are in the language of arithmetic, and for simplicity we conflate numbers with numerals and sentences with Godel numbers. Now asked at MO. Say that a sentence $\varphi$ ...
user avatar
2 votes
0 answers
73 views

Is there an axiomatic system for propositional logic that does not use modus ponens as a rule?

Is there an axiomatic system for (classical) propositional logic that does not use modus ponens as a (primitive) rule? I would be particularly interested in a derivation of it from some other set of ...
user avatar
  • 105
0 votes
1 answer
56 views

Types of Logic/ proofs

I am having a hard time understanding the difference between classical, constructive, predicate, intuitionistic and propositional logic. I know that propositional logic studies ways of joining ...
user avatar
4 votes
0 answers
58 views

Are soundness and completeness a part of proof theory, model theory or something else?

I have a question that I hope can clarify the scopes of model theory and proof theory. I have the following naïve understanding of the two areas (please correct me if I'm wrong): Model theory is ...
user avatar
  • 61
1 vote
0 answers
44 views

Prove that propositional Aczel slash is closed under deduction

I have already proved that $ \Gamma |\phi \Rightarrow \Gamma \vdash_{IPC} \phi $. On the other hand, I have tried to prove the other side. I used induction on the length of the proof.(I used natural ...
user avatar
2 votes
1 answer
84 views

How exactly are you allowed to use free set/predicate variables in first-order arithmetic?

In first-order arithmetic, you can't quantify over sets of numbers. However, you can include sets as free variables. I don't think this is just a meta-linguistic thing, as I've read papers about Peano ...
user avatar
  • 21
2 votes
4 answers
273 views

Why is Q → P a logical consequence of ¬(P → Q )

I don't want to ask my professor about this because I'm awful at this and he's not the, uhh, patient type of professor to say the least. Anyhow, it was my understanding that ...
user avatar
36 votes
3 answers
3k views

Under the Curry-Howard correspondence or loosely "proofs-as-programs", do we also have "programs-as-proofs" and what would some arb. program prove?

Curry-Howard Correspondence Now, pick any 5-30 line algorithm in some programming language of choice. What is the program proving? Or, do we not also have "programs-as-proofs"? Take the ...
user avatar
5 votes
2 answers
172 views

Prove that a construction exists: is this a constructive proof or existential proof?

This top answer claims that it is possible to prove that a constructive proof cannot exist. I think, if "non-existence of constructive proof" can be proven, then for some other questions, it ...
user avatar
  • 2,944
1 vote
1 answer
174 views

Natural Deduction Proof search algorithm for Classical Propositional logic?

I know of two algorithms for determining classical propositional validity: Convert the problem into a SAT problem, run a SAT solver. These algorithms are efficient, but it seems difficult/infeasible ...
user avatar
2 votes
1 answer
73 views

What is the relevance of the fast-growing hierarchy in the definition of Yudkowsky’s number?

I’m struggling with a certain connection the author draws in defining a certain “huge” number. The number is defined as follows: Let T be the first-order theory of Zermelo-Fraenkel set theory plus the ...
user avatar
0 votes
1 answer
41 views

Finding an Example for the following claim in Propositional Calculus?

Let $\Sigma$ be in $WFF$, we say $\Sigma$ is closed if for every $a$ in $WFF$ if $\Sigma \vDash a$ then $a$ in $\Sigma$. Claim: For every $\Sigma_1, \Sigma_2$ in $WFF$ such that $\Sigma_1$ is closed ...
user avatar
  • 21
1 vote
0 answers
55 views

How to prove the tautology $\neg\exists x\varphi\leftrightarrow \forall x\neg \varphi$ according to Halbeisen and Krapf's book

I'm studying some basic features of Proof Theory in the recent "Gödel's Theorems and Zermelo's Axioms", by Halbeisen and Krapf. In this book, the authors introduce a list of logical axioms ...
user avatar
3 votes
1 answer
63 views

Clarification regarding substitution in sequent calculus

Wikipedia's Sequent Calculus article states: $A[t/x]$ denotes the formula that is obtained by substituting the term $t$ for every free occurrence of the variable $x$ in formula $A$ with the ...
user avatar
  • 1,059
3 votes
1 answer
81 views

What are the syntactic restrictions on proof by contradiction?

I am reading Natural Logic by Neil Tennant and I am met with this example of proof by contradiction. It bothers me that the premise ~Ga was introduced seemingly ...
user avatar
4 votes
0 answers
55 views

Gaps between intutionistic and classical arithmetic

Let $\mathrm{I}\Sigma_n$ stand for the classical theory of Robinson arithmetic + bounded induction + induction on $\Sigma_n$ formulas. Let $\mathrm{CI}\Sigma_n$ stand for the intuitionistic theory of ...
user avatar
1 vote
1 answer
40 views

If a metatheory proves consistency of a theory, will consistency of the metatheory suffice?

I'm going to call a metatheory reasonable if it's consistent and whenever there exists a proof for a sentence $\phi$ from a theory $T$ the metatheory proves $T\vdash \phi.$ Suppose that some ...
user avatar
  • 3,695
2 votes
0 answers
44 views

What is quantifier-free induction over initial segments?

I am currently reading the section on Gentzen's Consistency Proof in this article on Proof Theory from the Stanford Encyclopedia. There it says: Given a natural ordinal representation system $\langle ...
user avatar
  • 903
4 votes
1 answer
135 views

Why do we need ordinal representation systems?

Trying to learn about ordinal analysis and I keep seeing the concept of the natural ordinal representation system, for representing ordinals as relations on N. In particular the definition of an ...
user avatar
0 votes
0 answers
35 views

Is the intuitionistic absurdity rule $\bot E$ necessary to prove that a theory $\mathcal{T}$ is consistent?

In Elements of Intuitionism (p. 145), Dummett wrote: Cut-elimination is directly connected with establishing consistency, and was so intended by Gentzen. Given the equivalence of N and L, acceptance ...
user avatar
1 vote
1 answer
73 views

Different textbooks, different formulations of the Deduction Theorem: sometimes the formula in the antecedent need to be closed, sometimes not. Why? [duplicate]

For clarity, let me take two examples: Shoenfield's Mathematical Logic, and Enderton's A Mathematical Introduction To Logic. Well, in those texts we have two different Deduction Theorems (we are in ...
user avatar
3 votes
0 answers
119 views

Open problems in Proof theory and Logic

There are numerous questions in the same form: "What are some open problems in mathematical logic". So for this we know: Shelahs "Logical Dreams" Logical Dreams Friedmans "102 ...
user avatar
1 vote
1 answer
93 views

How to derive $\prod x: \text{Nat}, Id(S(x), O) \to \bot$ in Intensional Type Theory

In HoTT Lecture, https://www.youtube.com/watch?v=VWmXF-P4-Z8&list=PL1-2D_rCQBarjdqnM21sOsx09CtFSVO6Z&index=7, Harper introduced a dependent form of recursion rule: $$ \Gamma \vdash M : Nat ~~~ ...
user avatar
2 votes
1 answer
72 views

When first encountering a set of primitive inference rules, how do we approach the derivation of the very first derivable inference rules?

I'm currently learning Ebbinghaus et. al.'s propositional calculus in their book Mathematical Logic, and I'm trying to derive the very basic rules of inference such as $\land$ introduction, the law of ...
user avatar
  • 698
0 votes
1 answer
149 views

An effective procedure to disproof Church-Turing thesis?

Suppose that an effectively axiomatized consistent formal system P that contains enough arithmetic for Gödel's Incompleteness theorems to apply, proves for any undecidable formula φ in the language of ...
user avatar
  • 3
1 vote
1 answer
96 views

Applying law of excluded middle to a theory-independent sentence

In $ZF$ (or $ZFC$) let's take a sentence $S:= CH\vee \neg CH$, where $CH$ is the continuum hypothesis. Then $S$ has trivial proof, namely application of the law of the excluded middle ($LEM$). On the ...
user avatar
2 votes
1 answer
55 views

Undo a weakened statement in sequent calculus later in the inferences

I'm working on an answer to (b) of Mathematical Logic, Ebbinghaus et. al. 1984 p. 64 Consider the following inference: $$ \frac{\begin{align}\Gamma \vdash A\\ \Gamma \vdash B\end{align}}{\Gamma \vdash ...
user avatar
  • 698
2 votes
1 answer
80 views

Are there any proof-size-aware logics?

I'm aware of provability logics which have a notation $\square P$ for "$P$ is provable", but I'm not aware of one which is more 'fine grained' and has a notion of proof term size (e.g. with ...
user avatar
  • 23
0 votes
1 answer
134 views

Proof of nonexistence of purely algebraic proof of the Fundamental Theorem of Algebra.

There have been questions before on Math SE about whether there is a purely algebraic proof of the FTA. But as far as I know, nobody has proven rigorously that there is no purely algebraic proof. Has ...
user avatar
  • 13.3k
1 vote
0 answers
114 views

Do all provable theorems have a finite number of proofs?

The Pythagorean Proposition states that there are 367 proofs of Pythagoras' theorem. Is there a limit for the number of proofs of this, or any, theorem? Are there provable theorems with infinitely ...
user avatar
3 votes
0 answers
53 views

Comparing two semantics, equivalent in the global sense, not in the local sense?

I am working on a project that involves a deductive system $\vdash$, with two model-theoretic semantics $\models_A$ and $\models_B$, for which $\vdash$ is sound and complete. That is, $\Gamma \vdash \...
user avatar
  • 317
0 votes
0 answers
36 views

Essential use of case analysis with theorem which is independent of ZFC

The continuum hypothesis ($CH$) is known to be independent of ZFC. Is it possible that some mathematical theorem $P$ has a proof of the form: ...
user avatar
0 votes
0 answers
82 views

What type of algebraic structure is logic?

What does Mathematica study? Answer: Structures; Sets where there are defined relations and functions. It happens that some of these structures contain others, and I think that logic is the structure ...
user avatar
0 votes
0 answers
32 views

A question on a specific kind of prenex normal form

We say that a first-order formula is in DNF if it can be obtained from a propositional formula in DNF by replacement of propositional variables with atomic predicate formulas. We say that $A$ is in ...
user avatar
1 vote
1 answer
49 views

Sequent type system in which all formulae are closed

In most presentations of the sequent calculus, the formulae that appear in a sequent $\Delta \vdash \Gamma$ may be open; i.e., may have free variables. I am looking for elegant presentations of ...
user avatar

1
2 3 4 5
19