This morning, for my own entertainment, I opened a separate account and posted a question entitled "Please Solve Quickly" mentioning that I was responsible for the proof of something and asked the public in general to solve it for me
Everyone was in such a hurry to delete it, I don't believe any of them noticed that what I had said what our professor had held us responsible for was in fact the proof of the Riemann hypothesis
I didn't vote on any of my posts though so it must be from something else
@DavidReed How do you know they didn't notice? I routinely close and delete such questions (about insincere attempts on open problems) and it gets boring after you see a thousand of them.
No problem. You can slowly read through the proof I gave LastIronStar yesterday of the semantic completeness theorem, starting from where he/she pinged you.
1. I never have used structural induction, despite my idea already have it implicit in mind (proving that each of the following: A or B, A and B, A implies B, not A are theorems, then every proposition is made of of these 4 pieces)
2. I forgot the base case where there are no boolean operators
3. I previously did not aware of the importance of the 2nd criteria to define the proposition P for the structural induction
Footnote to be explored myself much later: Semantic completeness (or not) of infinitary classical logic
Always forgot that due to that being the only proof that has Leaky's remark, which somehow disrupt my memory from remembering as "this can be derived" and "this is a redundant rule" conflict with each other in my brain
1. Repeat:
| A
|---------
| A
2. If-sub
|
|---------
| If A:
| A.
3. If-repeat
| A
| If B:
|---------
| A.
4. Implies
| if A:
| B.
|----------
| A => B.
5. Dual of implies
| A.
| A => B.
|-----------
| B.
6. And-create
| A.
| B.
|-------
| A and B.
7. And-destroy
| A and B.
|---------
| A.
| B.
8. Or-Create
| A.
|---------
| A or B.
| B or A.
9. Or-destroy
| A or B.
| If A:
| C.
| If B:
| C.
|---------
| C.
10. not-destroy
| not not A.
|------------
| A.
11. Contradiction
| If A:
e.g.0:
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]
e.g.1:
Q := A or ( A => B ) [short-hand]
Q is a theorem
Proof:
If not Q:
If A:
If not B:
Q.
not Q.
not not B.
B.
A => B.
Q.
not not Q.
Q.
@LastIronStar It's allowed, but calling him cruel is not a justifiable remark. If you think he is cruel, you can say so, but stating it as a fact is not justified. Also, if you were joking, I have nothing against you, but do not like jokes of any coarse nature or regarding the creator.
Well, firstly this has been around longer than Aristotle but let's not get into that. Secondly, are you saying this makes sense ONLY for everyday objects? Third, given a context, it is mutually exclusive na
@user21820 hmm, using the semantic completeness theorem on the sentence: not A and ( A or B ) thus showing it is a theorem, and then implies-Elim it to get B thus concluding it is redundant?
@LastIronStar Not only everyday objects, but at a fundamental level it does not make sense to talk about material. And they are not mutually exclusive. The cause of liquid water?
@DavidReed I refrained from using the word "god" because it is loaded with cultural and religious significance that people automatically assume when used.
@Secret Very colourful! If it helps you, good. But I can't really understand what's going on at the left...
@user21820 but just for my future reference, as I don't want to offend you, scrolling up it seems you don't like jokes like "god/lawmaker is cruel", is that correct?
@user21820 I have no idea how to illustrate the false sentence B and not B which is the feature of the contradiction rule. If two letters are in the same box, it means they are within the same context and if the box is gray, it means it is a subcontext
@LastIronStar That was not how I interpreted "context". As you can see, when I say "context" I mean situation. Not "the way we want to discuss it".
If your "context" means the way we choose to discuss liquid water, then the whole discussion becomes subject to our viewpoint, which is not how I think of cause and reason.
Anyway let's get the logic thread settled first. =)
@Secret Well that's why the Fitch-presentation seems better. Because it can distinguish between what you have and what you temporarily assume.
If you want, you could perhaps do the same in a diagram, but at some point it becomes suited for your own use.
btw, do fitch style proof had any relation to type theory, since the notion of context behave almost like a type with the outermost context being the universal type?
But for reference, one such presentation of a sequent-style calculus for first-order logic that is more similar to our Fitch-style system in its content is in sections 1.4 and 3.1 of Rautenberg's concise introduction to logic.
It just refers to the use of indentation and contexts.
In other words, it is a syntactical style and whatever semantics you wish to imbue on it is up to you. You could think of the global context as some type of all possible situations, and that a subcontext is just a subtype.
Sometimes, I think that way.
This viewpoint works for classical logic, but fails for modal logic.
Anyway one step at a time. Do you understand the semantic-completeness theorem? It is the first major result.
Note that this theorem is a theorem in the meta-system, and not a theorem in the Fitch-style system we proved it for.
@user21820 If I understood correctly, the outcome of this theorem is we can show every tautology is a theorem, and that the proof of this theorem is possible because our formal system has sentence of finite length consists of finite number of boolean operators thus allowing us to do structural induction on it?
@LastIronStar Anyway it's a side-track, though an interesting discussion to be had sometime. My point is that your statement seems to convey that you think it is impossible to talk about situations that do not depend on the discussion of conscious beings. That's all.
@LastIronStar When I said I "showed" the semantic-completeness theorem, I was talking in natural language plus a bit of mathematical language. All that can be formalized in a suitable formal system, which we call meta-system.
It's not important to know what the meta-system is now, except that my proof can be done. Modern logicians use ZFC as meta-system. I prefer something that seems more meaningful to me, such as predicative higher-order arithmetic, so if I use anything weird like ZFC I will say so explicitly. Again, not important to know the details right now, except that we are outside the Fitch-style system and reasoning about it. The structural induction that we used is also outside.
I thought the only outside thing we used is the applicability of Structural Induction - which was sort of explained away by appeal to semantic common-sense
Other things that are outside are the notions of arbitrary propositions and their sizes (which are natural numbers that are also outside) and our definition of semantics.
Notice one "and" is a boolean operation in the language of the system. The other "and" is outside in the meta-system (relying on our grasp of English "and").
This dependency on English can be removed simply by translating the whole thing into a suitable meta-system, where the outside "and" would be simply a symbol in the meta-system.
But again, whether the meta-system makes sense or not is something you can only judge by appealing to your natural language grasp of boolean operations.
@Secret NL: That statement about the meta-system is made in natural language. There cannot be proof of anything in natural language. To be precise, as I did so before, I will once again use "NL" or "MS" to specify when I am talking in natural language or the meta-system.
NL: Until you both grasp the idea, I could continue being this precise.
NL: After we define MS by explaining the syntactic rules, we can then work completely inside MS and everyone can check that our proof is correct, so as long as they accept MS as meaningful in whatever sense then they are forced to accept our theorems in MS as meaningful in that same sense.
NL: So I guess the answer is "no but good enough for practical purposes".
MS: Let Atom be an infinite set of symbols. We call f a truth assignment on atoms iff f is a function from Atom to {0,1}.
NL: "so as long as they accept MS as meaningful in whatever sense then they are forced to accept our theorems in MS as meaningful in that same sense." - well, if they find their construction of meaning, in whatever sense, is inconsistent - in that a later theorem doesn't make sense in the same method of meaning construction either they have to reject the original meaning construction or they have to reject MS!
NL: (Unrelated) I noticed the fitch style proof by me and Lastironstar on Q involves the exact same final steps (implication followed by contradiction followed by negation). Inspired from both backward thinking and also the notion of retrosynthesis in chemsitry, I am starting to wonder whether we can search for possible proofs of a given proposition by working backwards using the rules. There might be less possible routes for that thus giving us an idea on how constrainedthestructureoftheproofis
@LastIronStar NL: Yes! That is why people rejected naive set theory because it proved a contradiction.
@Secret NL: The most efficient way is to work both forwards and backwards. I didn't show you the other approach of proving the semantic-completeness theorem but it essentially does that.
MS: Let Prop be the set of all strings of symbols that are the closure of Atom under the following maps: ( str x ↦ "¬"+x ) , ( str x,y ↦ x+"∧"+y ) , ( str x,y ↦ x+"∨"+y ) , ( str x,y ↦ x+"⇒"+y ), where "¬","∧","∨","⇒" are symbols that are not in Atom.
NL: Note that this is still semi-formal; I will not attempt to translate this further to symbolic sentences in MS. But you should get the idea.
MS: We call g a truth assignment on propositions iff g is a function from Prop to {0,1} such that for any x,y in Prop we have ( g("¬"+x) = ( 1 if g(x) = 0 ; 0 otherwise ) ) and ( g(x+"∧"+y) = ( 1 if g(x) = g(y) = 1 ; 0 otherwise ) and ...
@LastIronStar MS: Given any collection S and collection of functions F, we call T the closure of S under F iff T is the minimal collection that contains S and is closed under each function in F.
MS: Given any collection S and function f, we say that S is closed under f iff ( for every x∈S we have f(x)∈S ).
@Secret No. Please read the definition of closure and check again.
NL: If MS is sufficiently powerful then we get the following:
MS: Given any collection S and collection of functions F, there exists a closure of S under F.
NL: You said that Atom is an infinite set of symbols, and an atom is a prop, but then you also said "¬","∧","∨","⇒" are not in Atom. This makes me wonder what are the remaining symbols that is needed to form a closure to give Prop?
@LastIronStar Correct. And I think it's now okay to stop using "NL" for NL. Every practical MS knows about the natural numbers, and hence can use them as symbols. We could use the even natural numbers for atoms, and some of the odd ones for those boolean operation symbols.
But at least, I've also defined semantics for propositions. Even though MS is not aware of what those things we call truth assignments on propositions mean, it appears to us to reflect what we want.
Ok, so the correct picture is Prop is either an atom or strings formed by atoms and "¬","∧","∨","⇒", thus in the diagram, Prop and Atom should swap place (and then stuff in between is clear)
@LastIronStar MS: Given any collection S and collection of functions F, we call T the closure of S under F iff T is the minimal collection that contains S and is closed under each function in F.
Closure includes S but the image of f on S does not need to.
The closure in the above way would be Union { T[k] : k∈N }.
You can check that if you apply any of those maps to a member of T[k], the result will be in T[k+1]. Thus if you apply them to the union of all the T[k]s, the result will remain in the union.
This is how closures are constructed in most set theories.
@LastIronStar MS: Given any collection S and collection of functions F, we call T the closure of S under F iff T is the minimal collection that contains S and is closed under each function in F.
