@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:
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...
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.
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.
@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."
@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.
@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).
@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.
@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.
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
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.
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.
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?
@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.
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.
@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.
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.
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.
@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:
@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.
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).
@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
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:
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.
@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.
@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)
(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)
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.
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.
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.
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.
@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.
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.
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.
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?
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.
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.
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.
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.)
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.
@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.
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 "...".
@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.
Sometimes called proof by contradiction.
@Taroccoesbrocco: Hello and welcome back after a long time!
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
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 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.
should proving things about cardinalities be so lengthy? I'm currently proving that Given any A,B if A has has m elements and B has n elements then A times B has mn. And before that I have proved that if A cap B = varnothing then A cup B has m + n elements. First one was not so short already but in the second one I proved like 20 different propositions already. The bijection I'm doing is x from {1,..,mn} to (f(a), g(b)) where a,b are such that x = nP(a) + b where P is a predessor function
@famesyasd - Just from the sound of it, chances are your proofs can be shortened a bit, but often they can still be quite involved, particularly if you're working them out from scratch and don't have at hand any good lemmas to use.
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...
