Provas Lógicas · Dedução Natural

📋 SÍMBOLOS

¬ Negação | → Se...então

∧ E (conjunção) | ∨ OU (disjunção)

↔ Se e somente se | ⊥ Contradição

∀ Universal | ∃ Existencial

⚡ REGRAS BÁSICAS

MP P→Q, P ⊢ Q

~E ~~P ⊢ P

∧I P, Q ⊢ P∧Q

∧E P∧Q ⊢ P / Q

∨I P ⊢ P∨Q

∨E P∨Q, P→R, Q→R ⊢ R

↔I P→Q, Q→P ⊢ P↔Q

↔E P↔Q ⊢ P→Q / Q→P

PC [P ⊢ Q] ⇒ P→Q

RAA [P ⊢ ⊥] ⇒ ~P

🔧 REGRAS DERIVADAS

MT P→Q, ~Q ⊢ ~P

SH P→Q, Q→R ⊢ P→R

DC P∨Q, P→R, Q→S ⊢ R∨S

SD P∨Q, ~P ⊢ Q

CONTRAD P, ~P ⊢ Q

🌍 QUANTIFICADORES

EU (∀-elim) ∀x Px ⊢ Pa

IU (∀-intro) Pa ⊢ ∀x Px (a arbitrário)

IE (∃-intro) Pa ⊢ ∃x Px

EE (∃-elim) ∃x Px, [Pa ⊢ Q] ⊢ Q

🔄 EQUIVALÊNCIAS

DM: ~(P∧Q) ⇔ (~P∨~Q) | ~(P∨Q) ⇔ (~P∧~Q)

COM: P∧Q ⇔ Q∧P | P∨Q ⇔ Q∨P

ASSOC: (P∧(Q∧R)) ⇔ ((P∧Q)∧R)

DIST: P∧(Q∨R) ⇔ (P∧Q)∨(P∧R)

DN: P ⇔ ~~P

TRANS: (P→Q) ⇔ (~Q→~P)

IM: (P→Q) ⇔ (~P∨Q)

EXP: ((P∧Q)→R) ⇔ (P→(Q→R))

Quantificadores: ~∀x~Fx ⇔ ∃xFx | ~∀xFx ⇔ ∃x~Fx

∀x~Fx ⇔ ~∃xFx | ~∃x~Fx ⇔ ∀xFx

📖 REGRAS DOS EXERCÍCIOS

Silogismo Hipotético (SH): P→Q, Q→R ⊢ P→R

Silogismo Disjuntivo (SD): P∨Q, ~P ⊢ Q

Modus Tollens (MT): P→Q, ~Q ⊢ ~P