If (A ⊬ ⊥ entails A ⊭TT ⊥) then (A ⊨TT B entails A ⊢ B)

Press the right key for the next slide (or swipe left)

also ...

Press the left key to go backwards (or swipe right)

Press n to toggle whether notes are shown (no equivalent if you don't have a keyboard)

Press m or double tap to see a menu of slides

First we show that if \textbf{A}, ¬B ⊢ ⊥ then \textbf{A} ⊢ B .

(To do this, we show how to turn transform a proof of the former kind into a proof of the latter kind.)

Now assume that for all sets \textbf{A}, \textbf{A} ⊬ ⊥ entails \textbf{A} ⊭$_{TT}$ ⊥

Suppose that \textbf{A} ⊨TT B

Then \textbf{A}, ¬B ⊨TT ⊥

So, by our assumption, \textbf{A}, ¬B ⊢ ⊥

Therefore (by the thing we showed first) \textbf{A} ⊢ B

IfA, ¬B ⊢ ⊥ then A ⊢ B

...

¬¬B

¬Intro: 4-6

¬Elim: 7

Assume that for all sets A, A ⊬ ⊥ entails A ⊭_TT ⊥

Suppose that A ⊨ _TT B

(We want to show that A ⊢ B)

Therefore: A, ¬B ⊨ _TT ⊥

An argument is logically valid just if there’s no possible situation in which the premises are true and the conclusion false.

Suppose for a contradiction that A, ¬B ⊬ ⊥

Then, from the assumption, we would have A, ¬B ⊭ _TT ⊥

So: A, ¬B ⊢ ⊥

Therefore (by the previous result) A ⊢ B

So we assumed this.

And derived this.

So:

If A ⊬ ⊥ entails A ⊭_TT ⊥

then A ⊨_TT B entails A ⊢ B