@LastIronStar That will come later. These rules will only define what is called Fitch-style natural deduction system for first-order logic. There are different deductive systems for first-order logic, that will allow you to deduce the same theorems. Different formal systems can be built on top of first-order logic.

ok

In the past, all this was not clear to mathematicians, and they just used intuition rather than rigorous logical deduction. That is why there were a number of serious conceptual errors. In modern mathematics, the formal system accepted as the conventional foundation for mathematics is called ZFC, which is a formal system built on top of first-order logic.

But we will get to that later. Now we just want to devise rules so that we can deduce sentences that are true in every context.

@user21820 why is this being written down explicitly, aren't they just difference in notation the top and the bottom?

@user21820 i don't know what that means, since i don't know what is a context and what is not - namely the 'every' part

Every line is either a context-header or a sentence.

So in the earlier example:

> ok, I write the following proof:
    A.
> what is the context in which i will evaluate this proof?

It is not a proof. That is the point.

The rules do not allow you to write it.

how did you go from Rules to PSA?

I did not.

I said I start from scratch and will design rules for a logic system that will achieve the goal.

ok

I think you got distracted. There is only one goal.

i got confused because the example was a PSA

It's not a PSA. A PSA has assert statements and is in C style.

This is clearly not a C fragment, nor are there asserts.

It is allowed by the first 3 rules we had.

Just focus on the goal:

As I stated, to achieve this it suffices to ensure soundness of each rule:

ok got it

So, now to answer your remaining question.

so necessarily any proof must start with the second rule

Yes.

ok 'twas a sanity check :)

The difference between the top and bottom of that newest rule is just that the bottom is a single sentence. The top consists of some sentence stated within some context.

The rule enables us to convert that inner deduction into an outer statement.

so it is more for readability than anything else?

Actually, you will find later that without that rule you will not be able to deduce certain true sentences.

First a simple example:

If A:
	If B:
		A.
	B implies A.
A implies ( B implies A ).

I am not going to bother about rules for brackets. Just use your common mathematical sense about what brackets mean.

Accept?

@user21820 thinking

Note the soundness for this new rule is almost by definition of "⇒". If previously we could only write only sentences that are true in their context, then what this rule lets us write would be true in the current context.

(And I'm lazy to type the symbol in the proof so I typed "implies".)

yes got that

So agree this rule is sound?

If A:
    If B:
        A.

This is same as:

A implies ( B implies A )?

Well you can indeed think of it that way, if you already understand contexts that way.

The point is that we need the rule to allow us to deduce that.

Without the rule, it's all in [y]our head. Who knows what is right or wrong intuition?

@user21820 isn't definition of implies what is written above in rule for it?

@LastIronStar No. The meaning of "A implies B" is "If A is true then B is true". The rules concern what strings you can write (no meaning attached). You must distinguish between the syntax (strings allowed to write) and semantics (meaning you think they represent).

The semantics that we want tells us how to design the rules. But the rules know no meaning.

Just like the compiler does not understand the programs it compiles. It just compiles and succeeds (syntax correct) or fails (syntax error).

@user21820 I see, this is the subtlety that is captured by "in its context" bit in our ultimate goal!

@LastIronStar Yes "in its context" is semantics, but the rules govern the context-headers syntactically.

So, next rule?

go ahead

| A.
| A implies B.
|--------------
| B.

This one should be easy to agree that it's sound, right?

@user21820 yes, so soundness is a semantic check we use to confirm syntactic rules right?

@LastIronStar Yeap. We design the syntactic rules hoping to capture the semantic ideas we have in our heads. Soundness is indeed the semantic property we want our syntactic rules to have. We could easily devise nonsense rules, but they would probably be meaningless to us.

For example, the rules of chess are not meaningful in any sense other than being rules of chess. The rules we are devising here, on the other hand, are intended to achieve the lofty goal.

We can see that if every rule we use is sound, the whole proof will achieve the goal (only sentences that are true in their context). That is why we are so concerned with checking soundness of every rule.

So ready to go on? After the next two rules we will be able to write more interesting true sentences.

Yeah, I believe I understand it.

| A.
| B.
|--------------
| A and B.

| A and B.
|--------------
| A.
| B.

ok

In general, most rules in Fitch-style come in pairs, one to introduce a symbol and one to eliminate it. Here we have a pair for the symbol "and".

It's just a bit of side remark; not important to understanding logic.

correct?

Yes. This is a sound rule. But it turns out we won't need it.

that will come from explosion + or-elim

Yea. First we need the other rules for "or" and "not". I believe we can go faster now since you appear to have grasped the idea behind the rules.

| not A.
| A or B.
|------------
| If A:
|     not A.
|     A.
|     contradiction.
|     B.
| A implies B.
| If B:
|     B.
| B implies B.
| B.

Yeap.

@LastIronStar: LeakyNun already knows every bit of this, so it's expected.

what is expected?

@user21820 the last message pretty much gave it away

@LeakyNun It's expected that you can show that the rule is redundant given the rest.

But we haven't specified the rest, so...

@LeakyNun is this also a redundant rule?

| A.
|---------
| A or B.
| B or A.

| A or B.
| If A:
|   C.
| If B:
|   C.
|---------
| C.

@user21820 got it, the twin assertions matter here since the top one is asymmetric w.r.t A, B!

Yes!

$\dfrac {A \lor B \quad \quad \neg A} {\dfrac{A \lor B \quad \dfrac{\dfrac {A} {\neg A ~ A}}{A \to B} \quad \dfrac{\dfrac B B}{B \to B}}{B}}$

And the second one, called Or-Elim, is what LeakyNun was using just now.

@LastIronStar oh that wasn't a rule... I was performing a whole deduction

@user21820 I'm not familiar with the latest style I posted: could you proofread it?

@LeakyNun don't deductions always start with rule 2?

what is rule 2?

@LastIronStar He wasn't performing an actual proof.

@user21820 nicely eliminated the or...I wonder why it's called or-elim... :P

He was showing that the rule you suggested is redundant.

@user21820 huhn?

To do so, he had to show that in any context where the lines above your --- have been written, he could generate a proof to get to the line below your ---.

His proof uses other rules that I haven't yet told you, so I told him to be patient (but he didn't really get it).

right

@LeakyNun I'm not sure what system you're using here. Looks like missing a step. But please write down all your questions somewhere else and later ask me okay?

ok

Two more rules, and we have enough to play with.

@user21820 Please pause at the next natural place, i need to cook some dinner but don't want to leave here at an unnatural place!

Yes the natural stopping point is coming.

Okay three more then we are done.

| A.
| not A.
|--------
| False.

| not not A.
|------------
| A.

| If A:
|   False.
|----------
| not A.

@user21820 wait what does false mean syntactically semantically?

You mean semantically?

@user21820 sorry yeah.

It means any absolutely false sentence that you like.

If you want me to pick, let "False" denote "0=1".

but i don't know anything other than the soundness of these rules. Numbers are yet to be derived...

I thought that was also part of the deal

@LastIronStar Then just let "False" stand for a false sentence.

Any absolutely false sentence, meaning false in every context, just like "false" in programming.

Nothing fancy is going on here.

You know "false" in programming. Just use that.

@user21820 yeah but...

@user21820 so this is not obvious

If you really really don't like that, here is an alternative pair of rules to replace those three:

yeah i don't like it TBH

| not not A.
|------------
| A.

| If A:
|   B.
|   not B.
|--------
| not A.

No more "False"! But the lack of such a syntactic feature will come to bite you later.

It is the same as not allowing mathematicians to write the word "Contradiction" in their proofs.

Okay pick. Which variant you prefer? Both will give the same theorems (well almost), so I don't care which you want.

@LeakyNun: Footnote for you: Every propositional sentence that does not use "False" is provable by one variant iff it is provable by the other variant.

@LastIronStar: Quick pick.

Haha..

Whichever you pick, I'm going to have to justify its soundness.

@user21820 one sec

just processng

I think the two rule variant is closer to home.

Okay then we go with that.

First one of that pair is clearly sound, by our semantics for "not" (flip the truth value).

@Secret sorry if i'm picking it for you as well!

@LastIronStar Don't worry I'll explain why the other one is okay after we're done.

Second one is the only non-trivial rule in the whole collection so far.

@user21820 btw, we've not defined not

@user21820 I want to try my luck at its soundness

"flip the truth value"; namely "not A" is true iff "A" is false, but is false if "A" is true.

@LastIronStar Well before you try, I will say that actually I must specify a restriction on "A". It must be a sentence with a boolean truth value.

Then (I claim) the rule is sound.

aren't we assuming there is only two possible truth values from the outset of this exploration?

We do, but I actually didn't say anything about what A,B,C could be.

All the other rules will work fine even if they are junk strings. That additional restriction we need for this rule is what sets it apart from all the other rules.

Otherwise what it allows us to write could be meaningless.

this seems profound

my brain is not cooperating with me any longer, i will need a short break, is it close by?

Just go with your original assumption to establish its soundness. I'm just making that assumption explicit for this rule. After this is actually where we stop, because these rules are sufficient to prove every propositional sentence that is true in every context!

btw not also assumes boolean truth values

@LastIronStar Not really. The first rule in the pair only says that if we can write "not not A." then we can write "A.".

And you will find that the only time you can write "not not A." is when "A" is boolean. =)

yes, i was just gonna say that not not is well-defined only for boolean

The reasoning for soundness of the second rule in the pair is just the same reasoning that I made you use to analyze the program. Even though this has nothing explicitly to do with programs now.

Do you see it, or do you want me to just tell you?

@user21820 I can see it, but i'm not convinced by my intuition

basically it seems to hinge on an assumption that B and not B both can't be at the same time

Am I starting to lose it?

Yes that is right. To justify that this rule is sound, observe that if each of the previously written lines is true in their context, then it must be that "A" is not true, otherwise both "B" and "not B" would be true in their context and their context holds!

Since "A" is a boolean-valued sentence, it must therefore be that (in the current context) "A" is false.

So the rule is sound. If you really want to be picky, you have to do this reasoning for each application of this rule in order from first to last.

so we assume that B is boolean as well?

No we do not have to assume that because we can only write down true sentences in its context. So if we could write "B" then "B" must be true.

For the sake of rigour, I have to expand on my picky comment. We have a finite sequence of deductions, each allowed by some rule. At first, we do not know whether this new rule (Not-Intro) is sound. But we know from earlier that all the other rules are sound. So at the first application of Not-Intro we can use the above reasoning to conclude that we still only wrote true sentences in their contexts. Then we proceed to the second application of Not-Intro, and so on until we are done.

You can hence see, by induction or intuition, that Not-Intro is sound.

Not-Intro is the last rule you've given?

Yep.

I sort of get what you are trying to say.

basically we move backwards from the point of application of Not-Intro?

and since our sequence is finite, it has to end somewhere?

i.e., start somewhere to be precise

Well in my explanation, I moved forward from the start to the end of a proof that follows the rules.

You could argue top-down instead, but it's easier to intuitively accept the justification in the forward direction.

but Not-Intro is basically a comment on the context a sentence is in, how then can it be applied to conclude in a forward perspective?

Wait I think you missed the argument.

Oh wait I think I missed my own argument.

No need for this based on my definition of soundness of a rule.

Let me do it again.

Let me copy here the definition of soundness of a rule:

Ah I see why I'm going haywire. My definition of soundness of a rule is slightly too weak.

Redefine it:

> A rule is sound iff ( whenever it is applied to lines in which every sentence is true in its context, the lines it allows you to write is true in its context ).

This is what I really wanted; not sure why I wrote the other version. Sorry

Does this make sense?

@user21820 i think it can be phrased better...

i'm not getting what you're saying let alone the difference with the previous definition

We say that we apply the rule when the part above the --- matches some previously written lines, and the part below the --- is what the rule applied to them allows us to write.

So we can rephrase it if you wish:

> A rule is sound iff ( whenever the lines above the --- contain only true sentences in their contexts, then the lines below the --- contain only true sentences in their contexts ).

Is that clearer?

@LastIronStar: According to this definition, Not-Intro is sound. If "A" is true in the current context, then "B" and "not B" would be both true in the current context, which is impossible, and so "A" must be false in the current context.

@user21820 isn't the context same for top and bottom in a rule?

Yes it's what I just referred to as "current context".

To verify soundness, we need only consider situations where the lines above the --- contain only true sentences in their contexts.

@user21820 Ok so I am sort of getting it but I'm using the Not-Intro rule as a litmus test to understand the validity of this definition - this is potentially circular so not feeling secure about my understanding.

@LastIronStar The least circular way I know is to look at it in terms of the asserts in a program.

It is ultimately circular because we are strongly using the assumption that "A" is either true or false, and that it cannot be that "B" is both true and false.

@user21820 how does this observation make it circular?

as in the reason you've given for its circularity..

Well it's how we "use" those assumptions in our justification that the rule is sound that is circular. But a more concrete alternative is to check all 4 possible cases and conclude that in any case the rule is sound.

the alternative is unappealing since that would make it specific to boolean truth values but that's unavoidable given the requirement on A for the rule to be sound...it is just somehow unsatisfying

Yes indeed this alternative assumes B is boolean.

So too bad; you'd have to go with the less satisfying justification for now.

But note that most of modern mathematics is done in classical logic, where we only deal with boolean sentences.

So at least you should be satisfied that this rule works for conventional mathematics.

=)

well, I for one strongly believe that reason is fundamentally subjective so satisfaction is in some sense a great indicator of understanding and should be worth striving for. Having said that, I can appreciate the merit of "sitting on it"/"letting it ruminate"/...etc,.

@LastIronStar Well your subjective intuition is not a problem. Many people have wondered about these rules before.

Anyway, it's a good time to stop for now. We have all the rules to prove any absolutely true propositional sentence (one build from atomic boolean propositions and "and" and "or" and "not" and "implies"). Next time I will sketch the proof of this fact.

yeah, I would need a break to process this. Thanks for taking time to exposit patiently, hopefully, i'll get to return the favour one day :)

@LastIronStar No problem. See you next time! =)

bye @user21820 ttyl

btw i just remembered, qubits - quantum bits can be both 0 and 1 at the same time. It is only observation that makes the qubit "settle" into a value of xeither 0 xor 1!

hopefully we will get to discuss this observation at a more meaningful level sometime later on along the way. @user21820

@MatheinBoulomenos hi

hey