Questions tagged [formal-proofs]

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

527 questions
106 views

Prove 𝑃′⋀(𝑃⋁𝑄)→𝑄 - How?

I'm going a course in computer science math, and I came across an exercise that is the following: Use the rules of equivalence and/or inference to prove: $\lnot P \land (P \lor Q)\rightarrow Q$...
49 views

Is this an axiom or does it have to be proved?

a and b are positive integers and x is greater than 1. In Rudin principles of real analysis it is not given as an axiom but proving is seems difficult to me
44 views

Strength of Asymmetric Tautology/Reverse Unit Propagation in proofs

Given a set of disjunctions in propositional logic, they can be said to entail another disjunction D if the negation of D, when added as a set of unit clauses to the original set, yields an ...
70 views

Why, intuitively, are propositional resolution proofs so long?

I'm trying to gain an intuitive understanding of why propositional resolution proofs tend to be so long. As every essential prime implicant can be produced via resolution, intuitively I would have ...
119 views

Let $u$ and $v$ be vectors in $\mathbb R^3$. Let $V=\{au+bv \mid a,b \in \mathbb R\}$. Prove that if $x$ and $y$ are in $V$, then $x+y$ is in $V$.

I'm having trouble writing this a proof for linear algebra. Let $u$ and $v$ be vectors in $\mathbb R^3$. Let $V=\{au+bv \mid a,b \in \mathbb R\}$. Prove that if $x$ and $y$ are in $V$, then $x+y$ ...
390 views

Can we prove if ⊢ (α → β) and ⊢ (¬α → β) then ⊢ β in L0?

The system L0 is defined as follows: Axioms: A1 (α → (β → α)) A2 ((α → (β → γ)) → ((α → β) → (α → γ))) A3 ((¬β → ¬α) → (α → β)) The only rule of inference is Modus Ponens: MP From α and (α → β) ...