@Secret Yes! But that is not the only way.

Right, but at least I am clarified it is possible

Great!

To show that A or not A is a theorem
Proof:

if not ( A or not A ):
	not( A or not A ).  [If-sub]
	if A:
		not( A or not A ). [if-repeat]
		A. [If-sub]
		A or not A. [or-create]
	not A. [contradiction]
	A or not A. [or-create]
not not( A or not A ). [contradiction]
A or not A. [not-destroy]

Correct? @user21820

@LastIronStar Correct. Exactly the same as mine, except a slight re-ordering.

Now you see why it's important to do it yourself? =)

@user21820 I knew deriving proofs for yourself is important if you don't understand them at first glance. I just had a brain-fart I suppose.

Sorry about that whole thing

@LastIronStar There's nothing to be sorry about. It is easy to not realize the importance of such self-attempting.

You say you knew, but we're all lazy sometimes anyway.

=)

haha yes, lazy is functional at times just not this time (note the horrifying pun)

Very funny.

:P

So, @Secret: Have you got it yourself yet?

Not yet, still compiling...

What happens if remove these rules one by one, is there a hierarchy of how powerful each rule is?

as in, we didn't use the implies rule anywhere so arguably it is not required for certain types of proofs

@LastIronStar Yes! Each rule I gave is not redundant, so if you remove any of them you get a strictly weaker system (will prove strictly less theorems).

@LastIronStar Yes too! For certain types of proofs, we won't need certain rules.

what about the followup?

i.e., can we quantify their power using some sort of hierarchy?

@LastIronStar In particular, you can create a system from any possible subset of the rules, and you should expect that it will not be a linear hierarchy, meaning that there may be two that are incomparable; each one proves some theorem that the other does not.

But later later.

I need to go.

See you both!

ok, maybe a partial order is possible?

where the power set of rules forms the set of elements for comparison and if every theorem provable by element A is provable by element B, you say that A<=B

@user21820 ok, tc, ttyl.

@LastIronStar Yes it will be a partial order, with your specified order-relation.

Since you are interested, note that the rule that I said was special really does have a special importance in this issue. Namely, if you want to deal with apparently well-formed factual sentences, you are going to have to make explicit the requirement that the sentence we are dealing with has boolean truth-value.

You could read the section on Quine's paradox in this post (ignore the rest for now):

It gives an explicit example of a well-formed factual sentence in natural language that cannot possibly have a boolean truth-value.

But we will temporarily forget this when we move on to (classical) first-order logic, as there is little point to discuss these alternative logic systems now.

@LastIronStar: Anyway, I will need to go again, for much longer. Take care and see you next time.

Hmm...
If not (A or not A):                                [Given]
        not (A or not A)                             [If-sub]
        not (A or not A) or (A or not A)       [Or-create]
        If A or not A:                                 [If-sub]
            A or not A                                 [If-sub]
            If not (A or not A):                    [If-sub]
                not (A or not A)                     [If-sub]
                A or not A                             [If-repeat]

@Secret It is difficult to explain why essentially everything else will not lead to a proof of the desired theorem. Next time I will give a semi-rigorous reasoning to deduce how a proof of it must look like (if a proof exists at all). Remind me if I forget about it. Bye!

If not (A or not A):                 [Given]
    If not A:                            [If-sub]
        not A                             [If-sub]
        not A or A                      [Or-create]
        not (A or not A)              [If-repeat]
    not not A                           [Contradiction]
    A                                      [Not-destroy]
    A or not A                          [Or-create]
    not (A or not A)                  [If-sub]
not not (A or not A)                [Contradiction]

Yeah, I need to sleep now, will talk later

If you can fix that, the rest is correct.

@user21820 my professor calls nbg "No Bloody Good" lol

meanwhile: github.com/kckennylau/Lean/blob/master/nbg/nbg.lean