Skip to main content

Questions tagged [formal-proofs]

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

Filter by
Sorted by
Tagged with
2 votes
3 answers
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 ...
Hosein Rahnama's user avatar
14 votes
3 answers
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 ...
Princess Mia's user avatar
  • 3,029
29 votes
5 answers
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 &...
matt_rule's user avatar
  • 419
3 votes
1 answer
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 ...
NikS's user avatar
  • 1,034
1 vote
0 answers
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 ...
FirstTryBogoSort's user avatar
2 votes
1 answer
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 ...
categoricallystupid's user avatar
4 votes
1 answer
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 ...
categoricallystupid's user avatar
2 votes
3 answers
85 views

Proving $\exists x P(x) \rightarrow \forall x P(x)$ from $\forall x\forall y(x=y)$

Problem: Using identity axioms, prove $\exists x P(x) \rightarrow \forall x P(x)$ from $\forall x\forall y \, x=y$. So far: I'm quite stuck on where to even begin. Working backward, I know we want $P(...
categoricallystupid's user avatar
1 vote
1 answer
197 views

Considering $\Gamma \vdash \varphi$, is $\Gamma$ a set or a list?

As far as I know, most of mathematical logic textbooks state the Weakening Lemma: Let $L$ be a first-order language. Then, for any sets $\Gamma_1$ and $\Gamma_2$ of $L$-formulas and any $L$-formula $\...
Kijeong Lim's user avatar
3 votes
0 answers
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 ...
Poscat's user avatar
  • 175
6 votes
2 answers
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, ...
NikS's user avatar
  • 1,034
1 vote
1 answer
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 ...
John Davies's user avatar
-1 votes
1 answer
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 ...
dmnsns's user avatar
  • 1
0 votes
2 answers
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: ...
Red Banana's user avatar
  • 24.2k
1 vote
1 answer
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 ((((ψ→φ)→(¬χ→¬ξ))→χ)→τ)→((τ→ψ)→(ξ→ψ)) ...
xamid's user avatar
  • 258
3 votes
2 answers
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 ...
Rubids's user avatar
  • 83
2 votes
1 answer
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)$ ...
John Davies's user avatar
3 votes
1 answer
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: ...
Le Grand Spectacle's user avatar
1 vote
2 answers
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 ...
Jonathan Chang's user avatar
2 votes
1 answer
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 ...
yomath's user avatar
  • 140
4 votes
1 answer
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 ...
William's user avatar
  • 223
2 votes
2 answers
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 ...
Ifkele555's user avatar
1 vote
2 answers
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 ...
Inzinity's user avatar
  • 1,773
9 votes
1 answer
559 views

Deriving A, ¬A ⊢ B in a weak Hilbert proof system

I am asked to derive A, ¬A ⊢ B in the following supposedly weaker system: Axiom 1: $A \rightarrow (B \rightarrow A)$ Axiom 2: $(A \rightarrow (B \rightarrow C)) \rightarrow ((A \rightarrow B) \...
user245312's user avatar
0 votes
1 answer
84 views

adding axioms to K logic [closed]

Let $K$ be the modal logic extending classical propositional logic by adding the necessitation rule N: if $\vdash A$, then $\vdash \square A$ and the distribution axiom K: $\square(A \rightarrow B) \...
yehehhd's user avatar
  • 119
1 vote
0 answers
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 ...
amadecember's user avatar
2 votes
0 answers
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 ...
Ali's user avatar
  • 45
2 votes
1 answer
232 views

I don't understand this definition of a derivation

Here is a definition of a derivation How can we, for the first time, obtain a derivation with a hypothesis to use, for example, $(2\rightarrow)$? More specifically, to prove, for example, $\vdash\phi\...
Seeker's user avatar
  • 347
5 votes
0 answers
211 views

How do I play type theory? What are the rules?

What I (think) I know: Type theory is a game where you construct trees from strings. As far as I can tell, the rules of the game are roughly those of a Gentzen system whose "propositions" ...
R. Burton's user avatar
  • 5,040
0 votes
0 answers
89 views

Proving that If $\lim_{h \to 0} \frac{a^h-1}{h}=1$, Then $a$ = Euler's Constant

I want to prove that if $$\lim_{h \to 0} \frac{a^h-1}{h}=1$$ then $a$ must equal Euler's constant, denoted as "$e$." However, I have some specific constraints for this proof: 1.$e$ is ...
uggupuggu's user avatar
  • 457
1 vote
2 answers
336 views

Can we use the proof of the weak Goldbach conjecture to also prove the strong Goldbach conjecture?

Why doesn't proof of the weak Goldbach conjecture also prove the strong Goldbach conjecture? Actually I am referring to this link. My question is why the logic used in this question cannot be used ...
Ok-Virus2237's user avatar
3 votes
0 answers
228 views

Is the weak Goldbach conjecture proved? [duplicate]

The Wikipedia page of the Goldbach's weak conjecture states that "In 2013, Harald Helfgott released a proof of Goldbach's weak conjecture. As of 2018, the proof is widely accepted in the ...
Ok-Virus2237's user avatar
3 votes
3 answers
227 views

What is an example of a proof that uses the principle of explosion/ex falso quodlibet?

I am reading through Mathematical Logic by Ian Chiswell and Wilfrid Hodges. In chapter 2 they introduce natural deduction rules. Before stating a rule, the authors (usually) motivate the rule by ...
Artyom Elessar's user avatar
0 votes
1 answer
67 views

Is this the proper method for finding the basis and dimension of a vector space?

I'm a bit new at linear algebra, so please bear with me. I'm trying to figure out how to find the basis and dimension of this vector space: U = { $(x,y,z,t)^T$| $x,y,z,t \in R$, x + 2y = 0, z − 3t = 0}...
James's user avatar
  • 73
0 votes
2 answers
113 views

Proving an if and only if statement using two contrapositive statements

I'm currently working on proving an iff statement and was wondering is it allowed for me to prove the two statements required to prove an iff statement using two contrapositive statements. (for ...
azozer's user avatar
  • 17
0 votes
1 answer
110 views

Examples of in ZFC, rules of inference and logical axioms

I was reading an introduction of ZFC set theory I found: https://ia803008.us.archive.org/31/items/A_C_WalczakTypke___Axiomatic_Set_Theory/Lecturenotes2006-2007eng.pdf Chaper 1 covers the idea of "...
Lab's user avatar
  • 635
1 vote
3 answers
79 views

How to write it formally? Convergence of an infinite sum

I know that the following sum $$\sum_{n=1}^{\infty} \frac{1}{\sqrt{1+2n}} e^{-\sqrt{n}}$$ converges because it's basically looking at $$\sum_{n=1}^{\infty} \frac{1}{\sqrt{n}} e^{-\sqrt{n}} \sim \int_{...
Mathick's user avatar
  • 318
0 votes
0 answers
63 views

How to generate iid random variables?

Suppose I want countable many $X_i$ that are iid to e.g the Gamma distribution $\Gamma(k,\theta)$. How do I actually construct these, given the usual definitions of random variables/measureable ...
SK19's user avatar
  • 3,161
0 votes
1 answer
49 views

Are there any ternary inference rules in propositional logic?

Every transformation rule I've seen in the context of propositional logic proofs have an arity of 1-2, with citations looking like ...
pinkboid's user avatar
0 votes
0 answers
148 views

Do order of lines matter when applying inference rules?

The wikipedia shows the form of Modus ponens as 1. If P, then Q. 2. P. 3. Therefore, Q. With 1 being the implication and ...
pinkboid's user avatar
1 vote
2 answers
213 views

Why is Simplification considered an inference rule instead of a replacement rule?

The wiki entry for Conjunction Elimination, sometimes called simplification elsewhere $$ {\frac {P\land Q}{\therefore P}} $$ is classified as an inference rule, rather than replacement rule. This ...
pinkboid's user avatar
2 votes
1 answer
267 views

Is my proof of $1+1=2$ correct?

Here is the proof: Note: I will denote the successor of a natural number $n$ by $(n++)$ If one assumes the Peano axioms then they may define addition as follows: $0+m:=m$ $(n++)+m=(n+m)(++)$ $\forall ...
Person's user avatar
  • 1,123
1 vote
0 answers
31 views

Interpretation of a proof by contrapositive in a small subset of the integers

So, i'm having a little problem on interpretating a result that i'm obtaining regarding a proof by contrapositive. Suppose we want to prove, by contrapositive, the following statements: Let $S$ = $\{2,...
Murillo de Godoy's user avatar
0 votes
0 answers
39 views

first order logic - Fitch Formal Proof Question

I'm doing this by myself over the summer and I'm really confused about construct formal proof with Fitch. Currently stucked on a problem that is asking me to derive Dodec(f) from Dodec(e), ¬Small(e), ...
Alice Chen's user avatar
2 votes
0 answers
88 views

Is the contradiction 1=0 a valid contradiction for a proof?

I am new to proper mathematical proofs and was attempting to prove: A prime number cannot be a perfect number. Here is my go: suppose n is a prime number. Therefore the only divisors of n, are n and 1 ...
Person's user avatar
  • 1,123
1 vote
1 answer
117 views

What is the difference between proving an equation versus verifying LHS = RHS?

I am referring to the book Mathematical Proofs: A Transition to Advanced Mathematics (3rd Edition) . In the chapter 4.4, I came across the following example - Prove ...
Parth Gupta's user avatar
0 votes
0 answers
56 views

If $\Sigma\vdash A \lor B$ then $\Sigma \vdash A$ or $\Sigma \vdash B$

I'm a new student for Mathematical Logic and I am trying to solve this question: In Hilbert proof system, prove or disprove the following: if $\Sigma\vdash A \lor B$ then $\Sigma \vdash A$ or $\Sigma \...
FAF's user avatar
  • 403
0 votes
1 answer
132 views

Help with Formal Proof using introduction and elimination rules

I need help with a proof where the premise is $\lnot A \land \lnot B$ and the goal is $\lnot (A \lor B)$. We are allowed to use the introduction and elimination of the following operators: $\lnot$,$\...
Meraz Hossain's user avatar
0 votes
1 answer
96 views

Advice on proof-based exercises and more theoretical math subjects [closed]

i am a soon to be graduate in physics and i am considering to do a master in the theoretical physics area, but i find myself a little bit "unfaithfull" of my mathematical skills. Let me ...
Lip's user avatar
  • 15
1 vote
0 answers
59 views

Reflection principle for finite subsystems of PA.

I would like to clarify the reasoning behind the proof of reflection schema for finite subsystems of PA that I found in "The Blind Spot" book. To be wore precise, we have a finite subsystem $...
A. G's user avatar
  • 338

1
2 3 4 5
18