@user21820 I know I have asked this many times, but I still can't get it: to me, somehow, incompleteness means that the system is aware of its axioms...
I was looking at your last post. Are you talking about the notion of completeness in a system or in a theory?
the "incompleteness theorem" would be a theory one
I'm trying to interpret your last statement
Thought I might be able to give some feedback in 820's absense
Incompleteness in this context means that there is a consequence of the theory not provable by the theory
I'm struggling to grasp what you are trying to say when you say "the theory is aware of its axioms"
Certainly not an issue if you would prefer to wait for his response. I know he has been more engaged in your progress than I have.
@user21820 I certainly hope you are referring to the "for fun" part and not the "impractical" part :)
@LeakyNun I should actually probably change my parlance to avoid contradicting frequently used definitions. Incompleteness in this context would mean there is a statement such that neither it nor its negation is deducible from the axioms
There is no semantics inherent in the notion of completeness of a theory, what I said initially was very bad verbage. Semantics is at the core of the notion of completeness of a logical system however, but that is not what you are referring to.
Yes I understand your meaning now
820 and I were just arguing about this yesterday :)
@user21820 I know I have asked this many times, but I still can't get it: to me, somehow, incompleteness means that the system is aware of its axioms...
Ah. Just to clarify I was talking about rejecting the monty hall problem (I know I kind of went off on a tangent there). I accept the incompleteness theorem in its entirety. Philosophically, I don't assign the meaning to it that you do, but I can understand how that would bug you.
I just view it the same as any other mathematical proof, I don't really assign any philosophical meaning to it one way or the other.
@LastIronStar You didn't say so, but I want to point out that it is a common mistake in popular science articles that quantum mechanics implies that the world does not obey classical logic. The fact is that the mathematics behind quantum mechanics (at least for qubits) is completely classical. What is true is that there may be different systems that capture qubits' properties more elegantly than the more powerful foundational system. Different systems may have (different) real-world interpretations.
That's all I want to say for now.
@LeakyNun Godel also has a completeness theorem. To prevent confusion, you should use semantic-completeness and syntactic-completeness for the two notions. In practice, if you are precise enough, they can be distinguished because the former is about the deductive system while the latter is about the formal system.
@LeakyNun The system does not know about itself.
@DavidReed: That is what you both seem to not be getting yet. I have some more examples to explain the distinction between true self-reference and what is happening here, if you want to hear.
@LastIronStar Hey, so just reviewing what you mentioned about qubits. 820 and I have actually discussed this in here before. The mathematics behind quantum mechanics (and superposition in particular) is very non-trivial and heavily dependent on functional analysis. Others might disagree, My personal approach is to not assign any real-world meaning to this other than it simply being a model that accurately predicts phenomena. Especially given the arbitrariness of its development.
My justification for that is that it is captured by a program as I showed you some time back, and the diagonalizing program on any given input enumeration literally produces a sequence that does not refer to itself but is simply not among those enumerated. Since neither the program nor the output is in any way recursive, nothing here is self-referential.
@user21820 Occasionally My nucleus accumbens has been fried from recreational drug use. In order to focus in general and be functional I have to take some very unusual medications. Occassionally I will discontinue them to keep my tolerance from getting to high, during this period I generally have difficulty focusing/processing things. It comes and goes, at present I am feeling very light-headed and is very difficult for me to think at this level of abstraction.
I am also a little exhausted from our exchange yesterday, would you mind if we continue this particular conversation another time?
@DavidReed And if you don't mind me being blunt, I would advise you to stop recreational drug use if not for medical purpose. I know it may give a good feeling, but it is not a well-founded one, and the consequences may not be worth the temporary feeling. If you find my this remark to be offensive, then sorry please ignore 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 ).
A rule is sound iff ( whenever it is applied to lines rules in which every sentence is true in its context, the lines it allows you to write is true in its context ).
> 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 ).
@user21820 are the contexts being referred to here same or different? as in I can establish a subcontext above ---------, and another subcontext below --------- so which context(s) are we referring to respectively?
@LastIronStar Every sentence has a context, which can be read off the proof structure by following the indentation, and just collecting all the context-headers that 'govern' that sentence.
@user21820 ok so they can be different contexts then?
@DavidReed If you are talking about the qubits thing - there was no discussion before that, so don't worry about it. if it's about the logic discussion, i'm not sure which comment you are referring to
@LastIronStar I think the answer is yes, but I'm not sure what your question is, so let's just use a concrete example.
If ( A or B ) and not A:
( A or B ) and not A.
A or B.
not A.
If A:
A.
not A.
If not B:
A.
not A.
not not B.
B.
If B:
B.
B.
( ( A or B ) and not A ) implies B.
So every rule can be used in any context, and if you have written what is above the --- in that context then you can write what is below the --- in that same context.
Soundness states that, for any two lines (in context C) that are of the form given above the ---, if "B" is true in its context (which is "C: If A:"), then "A implies B" is true in its context (which is "C:").
Of course, this rule only applies if the "B" really is underneath the "If A:".
@DavidReed No. It's about soundness of rules in a Fitch-style system.
@LastIronStar There will not be any issue with the last version.
If all the rules are sound (by this definition), then for any proof of length n, you just have to invoke soundness at most n times, one for each line you write according to some rule, and then you will conclude that every line is true in its context.
First I shall say again the definition of proofs and theorems in this system. A proof is a finite sequence of lines that can be written according to the rules. A theorem is a sentence that can be written in some proof under no context-header.
Precise people will call such proofs as Fitch-style natural deduction proofs.
Next, suppose we are only dealing with boolean atomic propositions and propositions formed from them using "not" and "and" and "or" and "implies".
So we will only write context-header "If A:" where "A" is a proposition formed as above.
This system is now what is called classical propositional logic.
And the semantics we had given to "not" and "and" and "or" and "implies" are exactly the semantics for classical propositional logic.
If ( A or B ) and not A:
( A or B ) and not A.
A or B.
not A.
If A:
A.
not A.
If not B:
A.
not A.
not not B.
B.
If B:
B.
B.
( ( A or B ) and not A ) implies B.
It is just a matter of definition. I defined a proof to be one that obeys the rules, so altering it in any way (even to insert a theorem that you have already proven before) may make it no longer a proof.
1. If A: 2. If B: 3. A. 4. B implies A. 5. A implies ( B implies A ).
Context: 1. U 2. U: A 3. U: A: B 4. U: B, A? 5. U: B, A (in that order)?
1. A. 2. A implies B. 3. -------------- 4. B.
Context: 1. U 2. U: A, B ? 3. (separator to indicate which rule it is) 4. U?
1. | not A. 2. | A or B. 3. |------------ 4. | If A: 5. | not A. 6. | A. 7. | contradiction. 8. | B. 9. | A implies B. 10. | If B: 11. | B. 12. | B implies B. 13. | B.
Context: 1. U 2. U 3. (separator) 4. U:
Also with this definition of soundness, how is it different from validity?
> 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 ).
Also, another interesting observation: when breaking down each lines by identifying the context of each line, it started to remind me of type theory
@LastIronStar Every sentence has a context, which can be read off the proof structure by following the indentation, and just collecting all the context-headers that 'govern' that sentence.
@Secret Paste, then click "fixed font", then send.
So just read off the proof structure to get the context. This is exactly as in Python, and in any case nothing essentially different from C/Java or other programming languages.
1. If ( A or B ) and not A:
2. ( A or B ) and not A.
3. A or B.
4. not A.
5. If A:
6. A.
7. not A.
8. If not B:
9. A.
10. not A.
11. not not B.
12. B.
13. If B:
14. B.
15. B.
16.( ( A or B ) and not A ) implies B.
Let U be the label for the outermost context, C be the label for the context "( A or B ) and not A". Then: Contexts: 1. U 2. U: C 3. U: C 4. U: C 5. U: C 6. U: C: A 7. U: C: A (A and not A in the context A, what does that mean, it seems more weird than a contradiction, which rule are we using to get from line 7 to line 8?) 8. U: C: A 9. U: C: A: not B 10. U: C: A: not B 11. U: C: A 12. U: C: A: 13. U: C 14. U: C: B 15. U: C (which rule we are using to get from line 14 to line 15?) 16. U?
Specifically for the question in line 7. How can there be a contradiction of something within the context of itself?
@Secret Who cares? That's why I said that all it matters is that we only write sentences that are true in their context.
@Secret Your contexts for each line are correct.
Did you read the whole conversation? You either need to check one line at a time that obeys this goal given that all previous lines obeys it. Or you need to just check that each rule is sound as I last defined it:
> 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 ).
So if we check the lines one line at a time to see if they obey the goal, then we are checking the validity, while if we check whether the rules being prescribed contains only true sentence in its context given lines before the --- contains only true sentence, then we are checking the soundness of the rules?
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.
Just slowly think through it. It ought to be easy to grasp. Informally, sound rules only generate true sentences from true sentences.
There's still something unclear about the rules applied in the specific cases covered (such as how is line 15 written), but the general concept, including the notion of theorem and proof is clear to me
1. Rules: Has a shape ... ------ ... where given any sentences ... above the --- in any context, we can write sentences ... below the --- in the same context. 2. Soundness: A rule is sound if given ... above the --- is true in their context, ... below the --- must be true in their context. This gives meaning to the rules hence a notion of semantics 3. Context headers: Context headers specify contexts that follow and is syntactically notated by indentation for our shape. It is commonly given by sentences of the form "If (sentence):"
0. Any rule | ... |----- | ... 1. Repeat | A |------- | A 2. Subcontext-creation (If-sub) | |------- |If A: | A. 3. If-repeat |A. |If B: |------- | A. 4a. Implication |If A: | B. |------- |A implies B. 4b. Implication two | A. | A implies B. |-------------- | B. 5a. And | A. | B. |-------------- | A and B. 5b. And two | A and B. |-------------- | A. | B. 6. Not | not A | A or B |---------- | B 7a. Or | A. |--------- | A or B. | B or A. 7b. Or two | A or B. | If A: | C. | If B: | C. |---------
Since user21820 have taught me how to deal with something like:
If A:
A
not A
I will be able to mentally convert that to False so that we will go through the stuff with the convention you are comfortable with, namely for any instance of False, it will be replaced with A followed by not A instead
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:
This is correct I think
@user21820 @Secret I think this is correct
the 11 commandments of Fitchism, twelve if you count the definition of how a rule looks
It does really felt that way after all those discussions which concludes with uncountable well orderings being quite ad hoc and is really the art created by Cantor
but anyway I am getting too far, let's get back to logic
I think uncountable well orderings will be an example of an abstract art, an art form that is even more narrow than fine arts. Even fine arts has some uses by the way it interacts with some audience in a real world relevant manner (social contexts), but abstract art is really just its own world that is absolutely detached with reality itself.
I don't quite get lines 2-4. Why is the context "A or not A" is false in the context "A". Or rather, I knew you are using contradiction in lines 2-5, but why we want to use contradiction, as having A to be true should not affect "A or not A"?
I just ignored everything but last two lines since not( A or not A) is never true...I think i'm committing several varieties of things that logicians would call sins
The point is that if you ever want to prove the theorem "A or not A.", you have to write a proof obeying the rules that has that sentence under no context.
line 7: Why do we want to do "not not", "A or not A" in context "not ( A or not A )" does not sounds false to me, the cannot force us to use the contradiction rule, or am I missing something?
Don'y pull me into this, I have not ignored your proof, I am confused by some bits of it. But either way, I will do what you said and write a proof, perhaps that will help me to auto clear my questions
@Secret is right - he has nothing to do with the way I stated my initial comment about the proof. If you don't want me to participate further you can tell me, I will leave the room never to return. I don't want to spoil even one person's chance of understanding.@user21820
It's just like programming. A teacher can talk all day about programs that he/she wrote, but if the student never tries to write his/her own programs and compile them without asking the teacher, it's going to be hard to grasp the concept. So try it out! =)
Attempt 1:
If not (A or not A):
If A or not A:
If A:
A or not A
If not A:
A or not A
A or not A
A
not A
A and not A
not (A or not A)
not (not (A or not A))
A or not A
Attempt 2:
If not ( A or not A ):
A or not A.
not ( A or not A ).
not not ( A or not A ).
A or not A.
Ok something's wrong in Attempt 2, because if this proof is sound, then it can be used to prove any negation
(I want to get inside the not, so I should use...)
If not (A or not A)
not (A or not A)
not not (A or not A)
A or not A
not not (A or not A)
A or not A
Lines 1-2 uses if-sub, lines 3-4 uses not-destroy, line 5 uses contradiction and line 5-6 uses not-destroy
I am not very comfortable with line 3 though, it seems like I did something that is not a rule by writing down "not not (A or not A)" out of thin air
When using the rule If-sub, I can write down any sentence inside the sub context. It does not have to be composed of sentence in the sub context, right?
@user21820 point is I am still not sure what I am writing is out of thin air or not. In particular, I am not sure what sentences I can write under some given sub context when using If-sub. Must they are based on the sub context in some way?
@Secret You have to follow the rules. If you cannot find a rule that justifies what you are writing, then no go. I already explained this before, but if you do not understand a particular rule, specify it.
@user21820 I'm not convinced this can be obtained by sequential application of rules, is it meant to be a parallel application? Or am I missing something?
so if my subcontext is A or B, then I can only write A or B, but cannot write A, and cannot write B? an if my subcontext is not C, then I can only write not C, but cannot write C?
@LastIronStar It is not a parallel application. That is why I said it would be painful to be 100% precise, but If-Repeat is supposed to allow the last line in your proof (given that B had already been written).
@Secret Yes. After all, for it to fulfill the goal, you had better not write things that are uncontrolled by their context.
@user21820 Ok, then I want to know why I can write B under the context A. Would it violate the requirement to only write sentences controlled by contexts?
The rule means that, if you have written every single line above the --- in that order in the current context, then you can write any line below the --- in the current context. In particular, if there is no line above the ---, then you vacuously can write any line below the --- in the current context.
The rule only applies if you have written ...
If you haven't written something of the required form, then you can't use the rule.
@Secret I never said anything about "control" in the rules, by the way.
