Text used in the minimal logic and principle of explosion video

minimal_logic.txt

This is the text used in the video

https://youtu.be/eeLa9tIhFMs

Minimal logic, or minimal calculus, is an intuitionistic and paraconsistent logic, 
that rejects both the Law of Excluded Middle (LEM) as well as 
the Principle Of Explosion (Ex Falso Quodlibet, EFQ).

# Classically via true and false proposition

Propositions A ... expression that functions as front or container for a truth value.
  Any proposition always is either a true or false proposition.
  Any proposition always is either T or F, the true or the false/absurd proposition.
  Any proposition always "holds" or "is mapped" to exactly one truth values,
  and there are two possible values, t and f.
    E.g.
    2+3==5 ... is T in Peano Arithmetic.

¬A ... is T if A is F and is F is A is T.
  I.e. functions as a unary function, flipping T and F.

A ∨ B ... is T if A is T and/or B is T.

A ∧ B ... same truth value as ¬(¬A ∨ ¬B)

A → B ... same truth value as (¬A ∨ B)

###

¬¬A (DNE) ... is same truth value as A.

A ∨ ¬A (LEM) ... is T (Consider either truth value for A)

((A ∨ B) ∧ ¬A) → B ... translates to ...
  ¬(A ∨ B) ∨ A ∨ B ... is T (Clear if A or B is true,
    but also if both are false.)

Ex falso quodlibet in words:
If A is true, then A ∨ B is true as well.
If also ¬A is true, then, using the above, B follows,
independent of what B is.
In summary, from (A ∧ ¬A) follows anything.

# Constructively

Propositions A ... expression that may be proven.

A → B ... is proven if assuming A, we have a means
  to prove B.
  Note: A not necessary "relevant" w.r.t. B.

A ∧ B ... is proven if we have a proof of A and a
  proof of B.

A ∨ B ... is proven if we have either a proof
  of A or a proof of B. In constructive logic,
  if we have the proof for A ∨ B, then we have also
  have one of the proofs!

¬A ... is proven if assuming A, we have a means to
  prove an "absurdity".
  Absurdity can be a constant or depend on context.
  ¬A ... can be written as as A → F

Note: ¬(A ∧ ¬A) (NON-CONTRADICTION) ... translates to
  ... (A ∧ (A → F)) → F.

###

¬¬A ... is proven ifwe have a means
  to prove ((A → F) → F))

A ∨ ¬A (LEM) is proven if we have a means to prove
  either A or (A → F).

((A ∨ B) ∧ ¬A) → B ... ?
If we have a proof for B, then it's certainly proven.
Else, what does (A ∧ (A → F)) give us except F?