12:26 AM
okay so it is not any set which has a bijection with S but only specific ones?

12:51 AM
@Secret I am sorry I have not finished typing up yesterday's post...but will within the next 24 hrs
@Secret Btw did I ever tell you about the FBI raid on my apartment?

2 hours later…
2:37 AM
@famesyasd Normally, in ZFC (using AC) we define #(S) or Card(S) as the least von Neumann ordinal that is in bijection with S. It is unique, so we can introduce # as a function-symbol. The basics are sketched in full here:
4

Counting has two purposes, namely for specifying sizes and indices. These are directly related for finite quantities, because the number of natural numbers (including $0$) less than $n$ (before the position $n$) is $n$. But in set theory, when generalizing to infinite sets these two notions becom...

2:55 AM
if $B \in \Delta$ then can we immediately say $\Delta \vdash B$ or is that not technically part of its definition

You can immediately say that. It's a proof from \Delta with only one step.

But where in our definition lets us do that
or is it more of an informal concept
as far as I could tell our only "move" involving $\vdash$ was modus ponens
if we have a set of known wffs containing $P$ and $P \to Q$ then via $\vdash$ we have proven $Q$

It follows exactly from the definition of proof for a Hilbert system that I've outlined before. A proof is a series of formulae that are either A) an axiom, B) in \Delta, or C) obtained from previous formulae in the series by modus ponens.

3:21 AM
@MaliceVidrine Is that the case though? In another answer someone had mentioned that assumptions cannot be part of a proof

That would mean you can't prove anything from a theory, so either that answer is wrong or has been misunderstood.

3

The theorem says that to prove an implication it is enough to assume the hypothesis and proceed to prove the conclusion. Proofs of that kind tend to be more natural than proofs that conclude the implication directly. Just as in regular mathematical practice: many theorems have the form "Assumin...

"Again, in mathematics you prove theorems. You cannot prove assumptions. In proofs, all steps are axioms or theorems. No step is an assumption."

@user525966 No you clearly have not understood the Hilbert-style system that you keep on wanting to study. There are two rules, one is an inference rule called modus ponens, which is as you described, and the other says that any axiom can be appended to the current proof.

@user525966 And you misunderstood this quote as well.

3:26 AM
I don't see what's misunderstood
He said "no step is an assumption"
and that they cannot be part of a proof

It says "all steps are axioms or theorems", exactly in line with what I just said.
His use of the word "assumption" is not the same as "axiom".

@MaliceVidrine's earlier comment: "It follows exactly from the definition of proof for a Hilbert system that I've outlined before. A proof is a series of formulae that are either A) an axiom, B) in \Delta, or C) obtained from previous formulae in the series by modus ponens."
\Delta in this case is the set of assumptions

@user525966 And this is the third quote you are misunderstanding, despite it saying the same thing.

It's not
Or at least the distinction isn't being made clear enough IMO

Well of course they are all variations of the same thing.

3:28 AM
We have one comment where we say a line in a proof can be an assumption, and another comment saying it cannot be

@user525966 Look, everyone uses a slightly different terminology. If you want to jump from one resource to another you are going to have to adapt to the differing terminology. If you want me to teach you, I will be consistent with my terminology, but I cannot prevent others from using the same words in different ways. Same with what MaliceVidrine wrote.
That is also why I do not want you to study logic first.
Because it is utterly confusing unless you already know how to use it.
MaliceVidrine's description separates between the logical axioms and the non-logical axioms (those in Δ), which he says is the set of assumptions but is not what I and some other authors would call assumptions.

I'll rephrase then:
If $B \in \Delta$ do you agree/disagree that it immediately follows that $\Delta \vdash B$?

@user525966 Yes, it follows from my very first comment, as well as your first quote's "axiom" in "axiom or theorem", as well as MaliceVidrine's case (B).

I do try to avoid the word "assumptions" for \Delta, even.

Aha.
So we actually have a more consistent terminology than it seemed.

3:33 AM
Which rule/concept permits jumping straight from $B \in \Delta$ to $\Delta \vdash B$?
Because as far as I can tell the only rule we have for $\vdash$ follows from our axioms or our rule of inference

Δ is the set of axioms, in the conventional terminology I am familiar with.

The set of "non-logical" axioms, as some people call them.

8 mins ago, by user21820
@user525966 No you clearly have not understood the Hilbert-style system that you keep on wanting to study. There are two rules, one is an inference rule called modus ponens, which is as you described, and the other says that any axiom can be appended to the current proof.
> any axiom can be appended to the current proof.
I don't care whether it has a name, or what you want to call it, but it is one of the rules of any Hilbert-style system.

@user525966 - notice that the one-term series "B" satisfies the criteria for a deduction of B. That is, it satisfies the criteria I list above, and its last term is B.

When I google around I largely see it referred to as the set of "assumptions", set of "hypotheses", etc. (e.g. www3.nd.edu/~cfranks/dt.pdf, mathworld.wolfram.com/DeductionTheorem.html, en.wikipedia.org/wiki/Deduction_theorem, etc)
non-logical axioms?

3:37 AM
@user525966 I am sorry but I as I told you people have different terminology. And many online resources that I have looked at are either wrong or very imprecise to the point of not being useful for a proper study.
I don't have time to read the ones you just linked, but you cannot assume that everyone is speaking the same language, even if there are no errors.

It's not just so much the word, it's that people are making different assumptions about what's actually proved/a valid proof/etc
For example how proofwiki.org/wiki/Deduction_Theorem says that if $B \in U$ then "obviously $U \vdash B$ "

They're not, is the thing. At least not if they're all talking Hilbert.

Whereas this www3.nd.edu/~cfranks/dt.pdf doesn't make such a step and instead goes straight to proving $A \to B$ by using $B$ from $\Delta$ with axiom I and modus ponens

@DavidReed no hurry, and no you have not

@user525966 There is no A and no B in that pdf.

3:43 AM
They're not assuming different notions of proof, they're just not going about the proofs in precisely the same way. And formally, in the second case, you can't prove that B \to (A \to B) and B\in \Delta yield A \to B without B already appearing somewhere in the proof.

They use $\varphi$ and $\phi$ and $\Gamma$ or something, forgot the exact symbols

So if they don't already show that \Delta \vdash B, they're just skipping an obvious step.
If anything, they're not using different notions of well-formed proof, they're using different notions of "obvious"

I guess I don't see why it's necessarily so "obvious" that if $B \in U$ then $U \vdash B$

@user525966 For the last time, that is one of the rules of the Hilbert-system.

if there's some formal proof of this or if it's more of an informal claim

3:46 AM
You don't get to say "no".

I don't see what you're referring to by saying "it's a rule"

Because as I've spelled out twice already, it comes from the definition of what constitutes a proof.

That's why I keep saying you actually do not know how to use logic at all.
And you will continue to have problems until you actually learn to use a deductive system.
There is absolutely no use in attempting to learn to analyze a system that you cannot actually use.

Where is this definition explicitly stated? I keep seeing things mentioned in this chat that don't appear anywhere on Google or in any of the texts I am finding
So forgive me if I am not so quick to blindly accept on faith here, I'm not seeing any kind of standardization and it's a little frustrating

There is no standardization. The reason we all can understand one another despite the plethora of inconsistent notions is that we know the underlying logical structure, because we know how to use logic.
But it has already been explicitly stated. Δ is the (non-logical) axiom set, so when they say a proof can use an axiom or modus ponens, that "axiom" refers to a member of the axiom set.

3:49 AM
Bell and Machover's "A Coure in Mathematical Logic" or Quine's "Mathematical Logic" both have precisely the definition I'm using. As do several other texts in my library.

I'm not convinced of this to the extent that most resources just call these "hypotheses" which on some level does make sense -- if we have a collection of assumptions (which may or may not be true), if one of our assumptions is false we may end up proving a false (or true) statement, hence the ex falso concept
so in practice yes we'd want everything to be true
but at least the alternative permits the use of proof by contradiction does it not?
which is one such valuable tool

@user525966 You say "in practice", which is what using logic is all about. In practice, yes we want all our axioms to be true under suitable interpretation. But you are mixing "in practice" with "in theory", which is what studying logic is all about.
Let me repeat myself; learn to use logic first. Don't waste your time on attempting to run before you can walk.
When studying logic, we consider systems where the axioms are arbitrary and need not be 'true' in any sense, just like chess has rules and initial setup that are arbitrary and have nothing to do with truth.
Analogously, right now you should not be studying arbitrary games including chess. You should be learning to just play by the rules of chess first.

Well so far I have yet to find the rule telling me why I can go from $B \in U$ to $U \vdash B$

You keep ignoring the answers we have both given you. Analogously you are asking why the king must move two squares when castling in chess.
The answer is, if you don't like that rule, don't play chess!

That's not the same thing at all

3:58 AM
That is where you are wrong. Every deductive system is just a rule-based system. There is no meaning whatsoever until we interpret it.

I'm asking where it's defined or what permits it, or how it follows

Nothing permits it.
We just like it.

You say it's a rule based system on one hand and then "it's not a rule / nothing permits it" on the other

I didn't say it's not a rule; you're changing my words.

So you say "nothing permits it / it doesn't follow from anything" but somehow it's still a rule?

4:01 AM
Can you for once just listen and think about what I say instead of ignoring? I said that a deductive system is just like game with rules. There is no meaning to the rules of chess, but if you want to play chess, you follow the rules.

I'm not changing your words -- I'm saying this doesn't make sense

Similarly, if you want to use a Hilbert system, you follow the rules.
There is absolutely nothing else to the deductive system.

I'm not ignoring you and I'm not saying I disagree with "meaning" -- the rules are precisely the thing I'm asking about
You say it's a game with rules, I'm asking what that rule is

I said it already twice now!!
37 mins ago, by user21820
@user525966 No you clearly have not understood the Hilbert-style system that you keep on wanting to study. There are two rules, one is an inference rule called modus ponens, which is as you described, and the other says that any axiom can be appended to the current proof.

4:03 AM
> the other [rule] says that any axiom can be appended to the current proof.
What on earth does this mean if it does not answer "what that rule is".

You say "you play the game, you follow the rules" -- yes, then what is the rule that says we can go from $B \in U$ to $U \vdash B$

Are you paying attention?

Oh my god.

"we just like it" is not a rule.

U is the axiom set.

4:03 AM
We keep answering that exact question.

You guys haven't actually answered it

> any axiom can be appended to the current proof.
Okay I know what your problem is.

How is "appending an axiom to the current proof" answering that question?

I gave a much more specific answer.

You failed to understand the goal of a Hilbert-system, and that is why you cannot see why we have essentially answered the question.
It's true; we didn't 100% exactly answer it.
Every conventional deductive system has rules that permit you to generate strings from a starting set of axioms. A Hilbert system has two rules: (1) generate a string that is in the set of axioms. (2) generate the string Q if you have already generated strings P and P+"→"+Q.
We say that ( S |− Q ) iff you can generate the string Q from the axiom set S.
Normally, we omit mention of the logical axioms L and write S |− Q instead of L ⋃ S |− Q.

4:09 AM
Yes, I agree, but when I see axioms stated I usually see $\vdash \text{axiom}$ or $\emptyset \vdash \text{axiom}$

Let me finish!!
So for example {P,Q} |− P∧Q, because actually we are saying L ⋃ {P,Q} |− P∧Q, where L includes all those (infinitely many) propositional axioms as well as first-order axioms if you are talking about first-order logic.
And by the definition I just gave, U |− P for any set of well-formed formulae U that includes P.
Okay that's it. Complete and precise. I don't care what others say, but this is Hilbert's system.
@user525966 When people write "|− Q" it should be interpreted (as per what I just said) as "L |− Q".
Okay I have to go. Please direct your further questions to MaliceVidrine.
One more thing I forgot to define.
A proof is a (finite) sequence of strings such that each can be obtained in one generation step (namely either (1) or (2)) from the previous strings in that sequence.
In particular, the first string in every proof must be an axiom, because you cannot use (2) since you haven't generated anything yet.
The sole reason for this notion of proof is so that you can mechanically check to verify a claim ( S |− Q ) along with a proof of Q from S, since each generation step can be mechanically checked. If you do not provide a proof, then it is potentially impossible to verify the claim because we cannot mechanically check all the infinitely many possible generation steps to figure out whether we can generate Q from S or not.
Okay that's it I think. I'm off now. See you next time.

4:26 AM
(Though I'm gearing down for sleep soon and am not nearly as good a teacher as 21820)

4:58 AM
This is starting to remind me of the surprise test problem

2 hours later…
7:19 AM
@Secret Indeed (C) is practically a soundness axiom, which in provability logic is the rule ( ⬜P |− P ). Of course, "certainty" is not the same as provability, so the correspondence may not fully hold. But you may be interested in the messages starting here:
May 17 at 5:41, by user21820
There are a few different dreams possible:
Note that I used (C) and (S) for completely different things than the article you linked. Their (C) is practically the same as my (D1*).

5 hours later…
12:15 PM
@user21820 I understand all of that, but it's not quite what I'm asking

2 hours later…
2:08 PM
@user525966 Sorry to say but I don't believe you know how to use logic, and that is why you still cannot see that both MaliceVidrine and I have answered your question. In particular, if you really understood what I said above, then I have explicitly and fully answered your question.
10 hours ago, by user525966
Well so far I have yet to find the rule telling me why I can go from $B \in U$ to $U \vdash B$
10 hours ago, by user21820
And by the definition I just gave, U |− P for any set of well-formed formulae U that includes P.
yesterday, by user21820
So I am going to give you homework. Use PA to prove the theorem I stated in Fitch-style or sequent-style. Once you can complete such proofs on your own, you will not only truly understand the nature of induction, but also you will see why the induction that is often done in introductory logic textbooks is nebulous and imprecise, because they often do not even set out the foundational system (or they do not adhere to it).
Sep 6 at 15:52, by user21820
@user525966: A good exercise would be to actually prove "∀k∈N ( ∃x∈N ( x·2=k ∨ x·2+1=k ) )" in the Fitch-style deductive system. Hint: Use that particular induction axiom I just wrote out.
Once I see your homework done, I will know immediately what you do and do not understand in using logic, and we can proceed properly from there.

You're saying for all k there exists some x that makes 2x = k and 2x+1 = k true, i.e. 2x = 2x + 1 or 0 = 1, which seems like either a very confusing or not helpful example

2:43 PM
@user525966 I don't know what you are saying. "∨" means "or", as you should know, not "and". Secondly, it appears you can't parse it right.
> for every k in N, there is some x in N such that either x·2 = k or x·2+1 = k.

ah whoops I definitely misread that symbol, my eyes aren't great
then yes makes sense, that's an or sign

Okay so your aim is to prove it formally within PA. Of course I advocate Fitch-style, but you are free to explore any other system, as long as you give me a link to a complete description of it.
As stated in the linked messages, you will need one of the axioms from the induction schema:
Sep 6 at 15:48, by user21820
Now the induction schema can be described. For each 1-parameter sentence P over PA, PA has the axiom "P(0) ∧ ∀k∈N ( P(k)⇒P(k+1) ) ⇒ ∀k∈N ( P(k) )". For example, for the 1-parameter sentence E = ( p ↦ ∃x∈N ( x·2=p ∨ x·2+1=p ) ), PA has the axiom "∃x∈N ( x·2=0 ∨ x·2+1=0 ) ∧ ∀k∈N ( ∃x∈N ( x·2=k ∨ x·2+1=k ) ⇒ ∃x∈N ( x·2=k+1 ∨ x·2+1=k+1 ) ) ⇒ ∀k∈N ( ∃x∈N ( x·2=k ∨ x·2+1=k ) )".
Informally, this is how one proves the desired theorem, namely "∀k∈N ( E(n) )", by induction within PA.

I see you're back, rehi @user21820

@AlessandroCodenotti Hi! I saw your question in the main chat-room but I don't know what it could mean.

I asked on main, that wiki quote looks very suspicious to me

2:55 PM
It sure does.

But it gave me the incentive to read about types and saturated models which I had been postponing :D

3:08 PM
@AlessandroCodenotti Ah nice. Unfortunately, I don't have much motivation to study modern model theory. I once took a course that got up to Morley's categoricity theorem, but I have forgotten half of the stuff already.
It's partly because I can't get a mental grip on a lot of the non-constructive constructions in model theory.

3:53 PM
@user21820 Again though this is running before I can walk -- this is getting into proofs of first-order logic and quantifiers and so on, that's a level beyond what I'm looking at currently
Let alone learning some fitch system which is a whole other layer on top of this
(nevermind the fact that it's unwieldy to type such a proof out in text when it seems like more of a graphical thing)

If you want to stick in propositional logic, then do these two:
Sep 18 at 11:33, by user21820
(1) ( A implies B or C ) implies ( A implies B ) or ( A implies C ).
Sep 18 at 11:34, by user21820
(2) ( A or B ) and ( B or C ) and ( C or A ) implies ( A and B ) or ( B and C ) or ( C and A ).
But you're getting it seriously backward; using first-order logic is much easier than studying even propositional logic.
But never mind; start with proving these two propositional tautologies in Fitch-style or sequent style.
You can type it in a separate text editor, and then copy and paste here, and click "fixed font" before "send". That is what all of us have been doing to display Fitch-style proofs correctly.
If you use sequent-style, feel free to write it on paper and upload a picture.

Why is first-order easier than propositional? Isn't it more or less propositional logic plus quantifiers?
Even when trying that example you posted earlier in FOL I don't see which axioms apply
Or what valid proofs look like in FOL (let alone propositional, hence my questions about what all these components are, how they're defined, what's valid, what's not, etc)
e.g. math.stackexchange.com/questions/9554/… -- “First‑order logic extends propositional logic with quantifiers”.

@user525966 I very carefully said "using first-order logic is much easier than studying propositional logic".
@user525966 Exactly my point; you are unable to use logic. And that is what you need to learn to do first, even before you move on to studying logic.
So right now, prove (1) and (2). For reference:
yesterday, by user21820
Feel free to ask me for help if you get stuck. But I want you to make a proper effort to learn an actual deductive system. You can use this Fitch-style system or this sequent-style system. If you use something else, you must provide me with a public link to a full description of all the rules. Read the linked messages for the axioms of PA.

What's (1) and (2)?
Those prop statements above?

Yes.

4:08 PM
Aren't those the ones you said were so massively ugly you didn't even want to get into it?
If so, why not use simpler examples?

They are ugly to prove in a Hilbert-style system. But easy in Fitch-style and not that hard in sequent-style. Other users in this very room have done similar exercises using the same system.
Look just do it instead of spending all your time trying to get away from actual work...

At least for me I see the whole using vs. studying as pretty interlinked -- even if I am using something, i'm often going "Wait, why are we even allowed to do that? What's going on in this step here? What lets us do that? What are these things representing? How are these things defined?" and we slip right back into trying to study what's going on

@user525966 I was doing precisely that with you in our first conversation, but you went off and never seemed to want to continue from where we left off.
And the fact remains that you still will have to learn to use it, so might as well focus on that part and get it done.

Because I can't continue from that point and I feel like you continually ignore it
Nevermind the fact you yourself said those examples were very messy (or however you phrased it)
I think using complicated example as a justification for skipping some easier step is a little misleading

You're wrong. We stopped here:
Sep 8 at 16:25, by user525966
will talk later then :) thanks again

4:13 PM
Are we talking about different things? What are you referring to?

There are two issues. Firstly, you have to learn to actually use a deductive system, so stop trying to wriggle out of it. Secondly, I will indeed justify why we are interested in the Fitch-style system I want you to learn, but that is a completely separate matter from you knowing how to use it.
And it may be counter-productive to do both together, which is what I tried to do in the first lesson but you never came back to finish that lesson.

I'm not trying to "wriggle out of anything"

Then just do (1) and (2).

forget it
You don't seem to be listening to what I'm saying to you

I am listening, and you are clearly not trying to learn what I want to teach you.

4:18 PM
Teaching what exactly? You're saying "do these two examples that I don't even want to touch with a ten foot fork myself"
To accomplish what? Assert that Hilbert systems are unwieldy? I already know that; it's not what I am trying to understand at this juncture

@user525966 For the last time, read what I said carefully:
9 mins ago, by user21820
They are ugly to prove in a Hilbert-style system. But easy in Fitch-style and not that hard in sequent-style. Other users in this very room have done similar exercises using the same system.
I can do them easily in Fitch-style, and that is precisely why I want you to use Fitch-style, so that you can actually learn to use logic.

I don't understand Fitch style
Even looking at simpler examples it doesn't really make sense
Let alone using it for a first order system that expands on prop logic

Then learn it! I can teach you, but you must be willing to drop all other systems temporarily and focus on this one!

So far I have only seen proof systems that use tables like these proofwiki.org/wiki/Law_of_Identity/Formulation_2/Proof_3
where they say "here are the lines, here's another line we can add by virtue of using MP with these other lines, or this axiom here, etc"

Just answer my question: Are you willing to learn Fitch-style or not?

4:20 PM
Willing yes but that post you keep linking makes no sense to me
Which makes me not even bother with it

@user525966 That's your mistake, because of course different people will need different amount of extra teaching to be able to understand and apply that post, and I am here precisely to provide that extra.
So if you are willing, we will go back to our first lesson, because that is what you need.
Summary:
Sep 8 at 15:56, by user21820
The programs I will write will use only bool variables, which are all input at the start of the program, and the rest of the program are composed of only boolean operations and if-structures and assert statements. Not even using else or return or anything else.
Sep 8 at 16:01, by user21820
For our convenience, we shall call this kind of restricted programs propositional programs or PPs for short. And we say that a PP is valid if it has no assertion error on every combination of inputs.
Sep 8 at 16:01, by user21820
Our goal will be to write only valid PPs.
Sep 8 at 16:15, by user21820
To achieve our goal, we shall devise a small number of rules to govern the kind of PP that we will write.
Sep 8 at 16:16, by user21820
And we want to do so in such a way that it is obvious why those rules will ensure that we can only write a valid PP.
@user525966: Do you remember the above?

do these functions "return" anything?
or are we just treating these as void functions with the goal of having them sail through without raising exception

@user525966 Yes. I am using C/C++ programming language as a crutch, and all we are actually interested in is the sailing through without exception.

Now consider the following PP:
if( P ):
...
assert P;
where the "..." is some arbitrary lines in-between. Suppose I tell you that there is no assertion error in the "...". Can you tell me whether this PP will have assertion error?

4:28 PM
it wouldn't

Sorry I forgot to use C syntax but you understood it thanks.
And your answer is right, and you are 100% sure of that.

I use Python too and that syntax would work there fine

That gives us one rule for writing PPs, namely inside any if-structure you can assert exactly the same thing as the condition of that if.

yes
What about putting things in the if-structure that are not asserted?

@user525966 That is fine. Just like you can have an empty if-structure and it will not have an assertion error.

4:32 PM
if(P and Q):
... #no assertion errors or anything to do with Q
assert P
#we don't assert Q or anything, Q only shows up in the if-statement

@user525966 This you correctly identify as a valid PP, despite it not asserting anything to do with Q.
However, we haven't stipulated rules that will permit us to write such a PP.

okay, so invalid PP's only occurring if we assert something not in the encapsulating if-statement?

@user525966 Could be more complicated than that. Let's just go on to a few other rules first.
Suppose you have the following PP:
...
assert A&&B;
assert A;
And I tell you that there is no assertion error up to "assert A&&B;". Can you tell me whether the whole PP will have assertion error?

no error

Right. More generally suppose you have:

4:36 PM
(assuming by "up to" you mean including A&&B)

Yes up to and including.
More generally suppose you have something like:
if(...)
{
...
if(...)
{
...
assert (A||B)&&C;
assert A||B;
}
}
And no assertion error up to and including "assert (A||B)&&C;". Again, can you see that the whole PP will have no assertion error?
No matter what all those "..." are?

no matter what? i mean doesn't it depend what's in the if-statements
if (A||B)&&C passes then so will A||B but maybe A and B are both false and don't appear in the if-statements
oh, no assertion error up until that point, forgot
then yes, no error

Right! Good that is the first key feature to understand.
The general form of the rule is that whenever we have an assertion of the form "assert P&&Q;" anywhere in a PP, we can write "assert P;" just after it and it will pass if the previous one passes.

yeah

Let's recap quickly. The first rule says that inside an if(P)-structure we can write assert P; and it will not fail. The second rule says that if we can write assert P&&Q; and it never fails then we can write assert P; immediately after that point and it will not fail either.

4:47 PM
I imagine this is meant to simulate things like P and Q infers P, P and Q infers Q, P infers P or Q, Q infers P or Q, etc.
yes

@user525966 You imagine right; this exact same reasoning will explain all the Fitch-style rules for "∧" and "∨".
But let's not get ahead too fast. There are two more important rules that have to do with if.
The first one is really simple. Suppose you have the following PP:
assert P;
...
if(Q)
{
... // if no assertion error up to this line
assert P; // will this line fail?
}

no
if assert P didn't fail the first time around it won't fail the second time around (assuming we're not changing variables here, since we mentioned we are setting them all at the start)

Good! So the rule we get from this reasoning is that you can always re-assert anything that you have previously asserted outside the current if-structure.
@user525966 Right; we are only writing PPs, which do not change any of the boolean variables (they are all input at the start).
Not surprisingly, in Fitch-style this rule is often called "restate" or "reiterate".
Okay now for the first complete example PP involving these three rules.
if(P&&Q)
{
assert P&&Q;
if(!P)
{
assert P&&Q;
assert P;
}
}
Is this a valid PP, namely no assertion error no matter what boolean values P,Q have?
And can you understand why the "assert P;" does not cause any assertion error?

yes because we only enter that first if statement if P and Q are both true, so we assert P&&Q (which passes) and skip the if(!P) block since P is true
doesn't matter what we put in that nested block since it won't get executed

Right. Observe that this PP obeys our three rules, the first assert comes from the first rule (assert the condition in the if), the second assert comes from the restate rule, and the third assert comes from the rule concerning "&&".
Now it is cumbersome to write all these rules out in English, and so we condense them into the following form:
if-subcontext:
|If P:
|-----
|  ...
|  P.
∧-elimination:
|P and Q.
|--------
|P.
|Q.
(Above I only used the one where you write P after "P and Q", but you can see it's the same reason you can write Q.)
if-restate:
|P.
|...
|If Q:
|  ...
|-----
|  P.

5:02 PM
So P. is short for "assert P"?

Right!
Can you see how what I have just written corresponds to the English descriptions of the rules, just now in non-C syntax?
I can explain if there is still any ambiguity.

I'm not quite sure what the -----'s represent

Sorry I forgot to say, the above format is used to mean roughly that if you can write what is above the line then you can write what is below the line.
And I have made a mistake. Should be:
if-subcontext:
|If P:
|  ...
|-----
|  P.

is that line the equivalent of $\vdash$?

@user525966 It is similar in flavour, but in Fitch-style all these rules apply even if you are inside some inner context (if-structure), so it will not be the same as what "|−" means in other systems.

5:09 PM
I think fixing that first example helped; I was not sure why the ....'s were below it
makes sense if I think of it as being able to assert stuff after the -----
based on the stuff above

Right.
I'm glad that you can understand this format, because it is not 100% precise but just serves as a short-hand for us to express our rules in a succinct manner.
Now have a look at this list of all the rules. Click on "(see full text)". In that list I omitted even the "...".

ok
saving these to a file or easier reference
If you don't mind I'd like to go through these and write equivalent PP's just so I can see if I get the idea

@user525966 That is an excellent idea that I would have proposed if you did not already. =)
Repeat just says you can repeat yourself again. We have just gone through If-Sub and If-Repeat and And-Elim.
After you finish writing the equivalent PPs, you should be convinced of all these rules. It turns out that these rules are all you ever need, and so you are done learning the rules for Fitch-style propositional logic.
The one people have the most trouble understanding is the last one, namely Not-Intro.
@Taroccoesbrocco: Hello and welcome back after a long time!
Unfortunately I have to go very soon.

1. Repeat:
| A
|---------
| A

assert A
assert A

2. If-Sub
|
|---------
| If A:
|      A.

if A:
assert A

3. If-Repeat
| A
| If B:
|---------
|     A.

assert A
if B:
assert A
4. Implies-Intro
| if A:
|     B.
|----------
| A => B.

if A:
assert B
A -> B

5. Implies-Elim
| A.
| A => B.
|-----------
| B.

assert A
assert A -> B
assert B

6. And-Intro
| A.
| B.
|-------
| A and B.

assert A
assert B
assert A and B
7. And-Elim
| A and B.
|---------
| A.
| B.

assert A and B
assert A
assert B

8. Or-Intro
| A.
|---------
| A or B.
| B or A.

assert A
assert A or B
assert B or A

9. Or-Elim
| A or B.
| If A:
|     C.
| If B:
|     C.
|---------
| C.

assert A or B
if A:
assert C
if B:
assert C
assert C
10. Not-Elim
| not not A.
|------------
| A.

assert not(not A)
assert A

11. Not-Intro
| If A:
|     B.
|     not B.
|-------------
| not A.

if A:
assert B
assert not B
assert not A

Correct! Pity programming doesn't have an "implies" operation, eh?

5:17 PM
some of these I am not quite sure I understand / not sure I understand how we're encoding A->B in the program

We can't, that's why I didn't say anything about it in the PP.
=D
Programming languages mostly don't have such an operation.
You can define it though: bool implies(A,B) { return ( A ? B : true ); }

do I need to wrap some kind of statement to show which part is the top and bottom
like say for the last one:
if A:
assert B
assert not B
#somehow indicate here that if everything above this point passes with no error...
assert not A # then this will execute without error
that rule is also weird in that we'll never reach that assertion (but I assume this is the point)

@user525966 For your own reference, yes do whatever you wish to indicate that, such as via your comments. But it's not necessary to post it here because you already understand it. =)
@user525966 It will never go inside the if A.

Or, actually, if A is false then that if-block never gets run, then not-A is asserted true
if A is true then we'll get an error with one of those two B assertions and we never reach the bottom

@user525966 Right! You finished typing this reasoning before I did.

5:22 PM
so how are we to interpret a situation where we never reach the bottom half of the bracket
i don't know how we call these
upper half of the bracket, lower half of the bracket

@user525966 If we follow the rules strictly, we would write a valid PP, and when you execute it you know it will run somehow and terminate, so it must reach the end of the program. It may not reach some lines though, and those are examples of "not reaching the lower half of the bracket".
This notation doesn't really have a conventional name, so I say below/above the line.
@user525966 Now I have to go, but you can in the meantime look at this two example proofs that another user did in this room using those rules.

thanks -- will look over

See you next time!

later