# Questions tagged [formal-proofs]

For questions about proofs within a formal system, such as natural deduction or Hilbert system.

853 questions
Filter by
Sorted by
Tagged with
164 views

### Negation of a Formula is Provable without Including the Formula as an Assumption

The following lemma states that if we can prove negation of a Well Formed Formula (WFF) $\alpha$ by assuming the formula itself, then we can do it without such an assumption. Lemma. Let $\Sigma$ be a ...
3k views

### Does every proof need an axiom saying it works?

I am wondering whether for every (valid) proof $P$ done in mathematics, at least one of the following statements are true: There is an axiom guaranteeing that its schema indeed gives us license to ...
• 3,029
5k views

### Are there statements so self-evident that writing a proof for them is meaningless? Is this an example of one?

Context: I know nothing about proofs and only a small amount about formal logic used in proofs. I'm trying to learn the basics of how to write a proof. For example, suppose I wanted to prove that &...
• 419
151 views

### On the limitations(?) of first-order logic in mathematical reasoning

Note: This is a follow-up to this earlier question. Also, for the purpose of this question, I'll use the term "normal mathematics" to refer to topics other than "foundational" ones ...
• 1,034
1 vote
74 views

### If proofs can be checked by computers, will we ever mistakenly believe a false proof? [closed]

As I understand, math proofs can be formalized and checked by a computer. Does this mean the math community will never have to deal with believing incorrect proofs? If not, is the issue with adoption ...
75 views

### Prove $\forall x\forall y \neg R(x,y) \wedge \neg \exists x\forall y\neg R(F(x),y)$ is a contradiction by natural deduction

Problem: Prove by natural deduction that the formula $$\forall x\forall y \neg R(x,y) \wedge \neg \exists x\forall y\neg R(F(x),y)$$ is a contradiction. So far: Here $R$ is a relation and $F$ a unary ...
119 views

### Prove $\forall x \forall y(xEy \rightarrow \neg x=y)$ in the vocabulary of graphs

Problem: Prove the sentence $\forall x \forall y(xEy \rightarrow \neg x=y)$ in the vocabulary of graphs using the axioms of graph theory. So far: The axioms of graph theory given are antireflexivity ...
85 views

• 143
102 views

### What kind of principles of reasoning can we use for classes in ZFC?

$\newcommand{\set}[2]{\{\ #1 \mid #2 \ \}}$ Motivation & Context In ZFC, everything in the domain of discourse is a set and we can only talk about classes in the metatheory. But we still want to ...
• 175
686 views

### Is "first-orderizability" a requirement for "legitimate" mathematical reasoning?

If we take a first-order theory (like $\mathsf{ZFC}$, or $\mathsf{ZFC}$ plus some additional axioms) as the foundation of mathematics, does that imply that mathematical reasoning (theorems, proofs, ...
• 1,034
1 vote
65 views

### Examples of sequent derivations that uses cut rule that can be modified to not to use cut rule?

The cut-elimination theorem states that any sequent calculus derivation that uses the cut rule also has a derivation that does not use the cut rule. I cannot find any explicit examples of such ...
• 589
85 views

### Formal proof of equality of ordered pairs [duplicate]

I am trying to prove with natural deduction the following with the Kuratowski definition of ordered pair: $$\forall x, y, z, w(\langle x, y\rangle=\langle z, w\rangle\leftrightarrow(x=z\land y=w))$$ I ...
111 views

### Proving $A\to (¬A \to B)$ with Łukasiewicz's axioms and modus ponens?

I am trying to answer the following exercise from Hao's Fundamentals of Logic and Computation: With Practical Automated Reasoning and Verification. Using only modus ponens and the following axioms: ...
• 24.2k
1 vote
106 views

### Smallest natural deduction proof for Meredith's axiom from basic rules

I tried to find a small natural deduction proof for Meredith's single axiom Infix notation Polish notation ((((ψ→φ)→(¬χ→¬ξ))→χ)→τ)→((τ→ψ)→(ξ→ψ)) ...
• 258
141 views

### Interpretation Theorem

The Interpretation Theorem is the following excerpt from Kunens old Set Theory 8. Appendix $1$: More on relativization We sketch here a more formal treatment than that in $\S 2$. There is a general ...
• 83
79 views

### Use sequent calculus to show if $\Gamma\vdash t_1=t_2$ then $\Gamma\vdash f(t_1)=f(t_2)$

Suppose the sequent $\Gamma\vdash t_1=t_2$ where $t_1,t_2$ are closed terms. Let $f$ be a one-place function symbol. I am trying to find a sequent calculus derivation of $\Gamma\vdash f(t_1)=f(t_2)$ ...
• 589
99 views

### Question about quantifiers in the proof of the cut eliminiation theorem

Lately I have been reading about the cut elimination theorem, I think I get the idea however I have been struggling with some technical details concerning quantifiers. Consider the following rule: ...
1 vote
90 views

### Basis for $V$ containing no elements of the proper subspace $U$

Let $U$ be a proper subspace of a finite-dimensional vector space $V$ . Find a basis for $V$ containing no element of $U$. We have no answer key for this question which i find annoying since that is ...
189 views

### What is machine-assisted formalization of proofs good for? And when to do it?

I have been watching Terry Tao's lecture on machine-assisted proofs https://www.youtube.com/watch?v=AayZuuDDKP0&t=1460s. However in terms of the formalization of proofs via systems like Lean or ...
• 140
485 views

### Are there axioms in a natural deduction system?

In the Hilbert system, a proof may include some axioms. In a natural deduction system, it seems no axiom is involved, at least from the examples I read in logic books. So, I wonder how axioms such as ...
• 223
169 views

### Natural deduction - prove a theorem

I am currently taking a course in "Introduction to Mathematical Logic" and I have been trying to do this proof, but everything I did just lead me to nowhere... Could anyone give me a ...
1 vote
167 views

### Circularity in the argument that Gödel's incompleteness theorems undermine Hilbert's program

I'm only familiar with the very basics of mathematical logic, but over the last few days I have been looking into Gödel's incompleteness theorems and it seems to me (but I might simply be grossly ...
• 1,773
559 views

• 119
1 vote
63 views

### Directly verify ring axioms for a ring with $2$ elements [duplicate]

I'm relearning mathematics from the ground up in order to keep up with it's rigor in the university I attend. I'm doing this with serge langs basic mathematics, which thankfully involves writing ...
158 views

### How to get comfortable with proofs includes algebra and inequalities

I'm self studying Baby Rudin and trying to do exercises, i got stuck at exercise 2.18 then looked up the answer from solution manual but the proof includes so much algebra for me to understand where ...
• 45
232 views

• 1,123
1 vote
31 views

• 403