CBL (The system your professor doesn't want you to see.)
Charlie-Boo
I. CBL: A Computationally Based Logic
The syntax and semantic of expressions in a CBL derivation.
II. Axiomatizations
III. Computer Science
The 10 Branches of Computer Science
IV. Solving Computer Science Problems
V. Program Synthesis
VI. Program Debugging
VII. Program Analysis
VIII. Programming Language Semantics
IX. Data Base Management System Query Processing
X. Theory of Computation (Turing)
XI. Recursion Theory (Kleene)
XII. Incompleteness in Logic (Godel)
XIII. Set Theory (ZF)
XIV. Paradoxes (Liar, Russell)
I. CBL: A Computationally Based Logic
Occam's Razor is a set of conditions and gauges by which we judge a
formal system. It states "entities should not be multiplied beyond
necessity". Thus, the smaller and simpler a system, the better.
It is unfortunate that computer science professors who publish on
theoretical computer science are attracted to long, complex systems.
Principia Mathematica is a 1,000+ page explanation of Logic. It is
said to be too long to be intelligible. Yet it is also called a great
work of Logic. They praise a system that directly contradicts
Occam's Razor for what constitutes a good system.
CBL is amazingly simple. In fact, consider Rosser's 1936 theorem, in
his paper, "Extensions of Some Theorems of Godel and Church".
Martin Davis, in his anthology, "The Unsolvable", describes
Rosser's theorem as being the strongest in undecidability, stating,
"Rosser relaxes Godel's requirement of w-consistency to simple
consistency. Clearly this condition cannot be relaxed further."
CBL provides what is clearly a simpler proof of Rosser's 1936 result
than anything ever published in the journals of Computer Science and
Logic. These periodicals and texts which describe Rosser's result
have provided 3 forms of proof:
1. Rosser's original proof showing how to construct a wff in Peano
Arithmetic that is not provable and not refutable. [Rosser-1936,
Margaris-1967,1990]
2. Showing a computer program from which we prove the theorem.
[Floyd/Beigel 1994]
3. Turing's proof of Rosser's result based on Turing's
unsolvability of the Halting Problem. [Turing-1937]
These 3 expositions take 5 pages, 1 page, and 10 sentences. CBL
provides a 1 sentence proof:
4. "If an axiomatizable system is consistent and decidable, then its
refutable sentences coincide with its unprovable sentences, but the
former is recursively enumerable while the latter is not."
This proof is formally generated by CBL. Indeed, historically CBL was
the source from which this amazingly ultra-simple proof was created.
CBL is a Computationally Based Logic. A traditional logic forms
statements concerning what is provable and what is true. CBL forms
statements concerning the characterization of certain mathematical
objects in a given base. The mathematical objects and bases can be
sets, relations or functions.
We characterize an object by giving a specific value which can be
substituted for a component in the base to form the object. The base
can be:
1. provable statements and expression substituted for free variables
2. true statements and expression substituted for free variables
3. true English sentences and noun phrases substituted for their
pronouns
4. computer programs (e.g. Turing Machines or PHP programs) and their
input and output
5. sets and their elements
6. classes and their elements
The general form of an assertion in CBL is:
M # P / Q
This means that value M characterizes object P in base Q. Then we
have:
P = Q(M)
For any given assertion W the assertion -W means that assertion W is
not true.
M is the specific value that characterizes relation P in base relation
Q. Consider the following 10 bases:
PR The provable sentences
DIS The disprovable (refutable) sentences
TW The true sentences
TS The true English sentences
YES The programs plus inputs that halt yes
NO The programs plus inputs that halt no
HALT The programs plus inputs that halt
DEC The decidable sentences
SE The sets and their elements
CE The classes and their elements
The mathematical objects P and Q can be of any form:
Relation (set) P(a)
Function f(a)
If any of M, P or Q is missing then the following is assumed:
M (exists M)
P set a
Q YES
For example, we have the following assertions:
M # P / Q M characterizes P in Q.
P / Q Q contains P, i.e., P can be characterized in Q.
P / YES P is a recursively enumerable relation.
P P is a recursively enumerable relation.
P / SE There is a set that contains just the elements of relation P.
P / TW P is expressible.
P / PR P is representable.
P / DIS P is contrarepresentable.
M # M M characterizes itself.
Using these assertions we can give facts concerning these various
bases, to axiomatize Computer Science.
II. Axiomatizations
An axiomatization (Axiomatic System) is any of the following equivalent
definitions:
1. There is a set of axioms (which are theorems) and rules of inference
(which map theorems to theorems) whose theorems are of the form given,
in this case a CBL assertion.
2. The set of provable sentences of a given form is recursively
enumerable.
3. There is a computer program that lists the theorems.
The result is to make a system of Logic:
1. Completely precise.
2. Able to be automated by computers.
3. Generalized by considering other values for its formal parts.
III. Computer Science
Computer Science is the science that studies the use of computers. The
Branches of Computer Science include:
1. PROGSYN Program Synthesis The creation of a computer program that
meets a given specification.
2. DEBUG Program Debugging To determine if a given program meets a
given specification.
3. PROGANA Program Analysis To determine the specification that a
given computer program meets.
4. PLSEM Programming Language Semantics How to create programs and
their specifications.
5. DBMSQP Data Base Management System Query Processing Solving queries
made against a data base of files that we decide to keep. E. F. Codd
developed formal systems to specify and manipulate data base management
systems.
6. TOC Theory of Computation Specifications that no program meets.
Alan Turing founded TOC with his 1937 proof of the unsolvability of the
Halting Problem.
7. RECTH Recursion Theory The study of programs that input and output
programs, including themselves. Stephen Kleene studied Recursion
Theory in the 1950s in an attempt to formalize Godel's Incompleteness
Theorems.
8. INC Incompleteness in Logic Limitations of Axiomatic Systems. Kurt
Godel founded INC in 1931 with his Incompleteness Theorems.
9. SETH Set Theory Axiomatization of what is an allowed set, to avoid
the contradictions in the paradoxes. ZF is the most common
Axiomatization of SETH.
10. PARA Paradoxes The Paradoxes are arguments that prove assertions
that we thought were not true. We can alter our earlier beliefs or add
the belief that the paradox is not a correct argument. Paradoxes
include the ancient Liar paradox quoted in the Christian bible, and
Russell's Paradox about the set of all sets that do not contain
themselves.
In general, we have the following relationships:
1. (Computer Program , Mathematical Object)
2. (Set , Element)
3. (Class , Element)
Each branch of CS considers one or more of these relationships. In
each, each component is either:
Input into a statement
Output from a statement
Exists according to the statement
This resembles the Predicate Calculus: statements that can be formed
using relations, not, and, or, there exists, and for all. However, we
also have Input and Output variables. So let us define the following
types of variables:
Input I, J, K, I4, I5, . . .
Output x, y, z, x4, x5, . . .
Quantified A, B, C, A4, A5, . . .
Then the basic problem in each branch of CS is:
1. PROGSYN
X # I / YES
For any given specification I, output the programs X that meet that
specification.
2. DEBUG
I # J / YES
Does a given program I meet a given specification J?
3. PROGANA
I # X / YES
What specification x does a given program I meet?
4. PLSEM
X # Y / YES
Show how to create programs and their specifications.
5. DBMSQP
X # I / J
Create the programs that solve a given query with given files
available.
6. TOC
- X / YES
Create the specifications that no program meets.
7. RECTH
X # X / YES
Create the programs that output themselves.
8. INC
- X / PR
What are the mathematical objects that cannot be represented in a given
logic?
9. SETH
X / SE
Create the mathematical objects which are characterized by sets.
10. PARA
- X / I
List all objects that we cannot characterize in a given domain.
Then the branches of CS are defined as:
PROGSYN X # I / YES Program Synthesis
DEBUG I # J / YES Program Debugging
PROGANA I # X / YES Program Analysis
PLSEM X # Y / YES Programming Language Semantics
DBMSQP X # I / J Data Base Management System Query
TOC - X / YES Theory of Computation (Turing)
RECTH X # X / YES Recursion Theory (Kleene)
INC - X / PR Incompleteness in Logic (Godel)
SETH X / SE Set Theory (ZF)
PARA - X / I Paradoxes (Russell)
IV. Solving Computer Science Problems
How do we solve these? In practice, we solve them as follows:
1. Q = YES
2. We solve X # Y / YES X # Y / YES PLSEM 4
"MUL-1" # MUL(I,J,X) * PROGSYN 1
"EMP-1" # EMP(X,Y) * DBMSQP
"s11" # s11(I,J) RECTH 7
"YIT-1" # YIT(I,J,K) * TOC 6
"f-1" # f(I) RECTH 7
M # P
N # Q
à
and(M,N) # P ^ Q
or(M,N) # P v Q
3. What do we do with the (X,Y) pairs?
What do we want?
a. (I,X) : If I=X then write X I # X / YES PROGANA 3
b. (X,I) : If I=Y then write Y X # I / YES PROGSYN 1
c. (I,J) : If I=X and J=Y then write "Yes" I # J / YES DEBUG 2
d. (X,X) : If X=Y then write X X # X / YES RECTH 7
4. We solve - X / YES - X / YES TOC 6
a. - ~P/P - ~YES/YES
b. - P / Q , R à P / Q : - R
If X = ~YES then write X
Q = YES
M # P is M # P / YES
P is M # P is M # P / YES
1. X # I / YES (Manna/Waldinger)
M # P(x) / YES
N # Q(x) / YES
union(M,N) # P(x)vQ(x) / YES
IF I = P(x)vQ(x) THEN X = union(M,N)
2. I # J / YES
"F x=0:1 W x" # TRUE(x) / YES
"1. x=0 2. write x 3. x=x+1 4. Goto 2" # TRUE(x)
3. I # X / YES
4. X # Y / YES
"F x=0:1 W x" # TRUE(x) / YES
5. X # I / J (Codd)
6. - X / YES (Turing)
- ~P / P
- ~YES / YES
- ~HALT / YES
- ~YES / HALT
7. - X / P (Godel)
- ~PR / PR
8. X / SE (ZF)
~TRUE / SE
That is, we have the following steps in proofs:
I. Axioms
A. M # P X # Y X # Y / YES
1. "s11" # s11(I,J) RECTH
2. "mul" # MUL(I,J,X)* PROGSYN , DEBUG , PROGANA
3. "EMP-1" # (eA)EMP(A,I)* DBMSQP
4. "YIT" # YIT(I,J,K)* TOC
5. "not" # not(I) INC
B. P / Q X / Y
1. ~TRUE / SE SETH (ZF)
2. ~TRUE / YES TOC (T1)
3. ~PR / TW INC (G1) - P , |-P , ~|-~P
4. DIS / PR INC (R1) - P , |-P , ~|-~P
5. DIS / TW INC (S1) - P , |-P , ~|-~P
C. P = Q
1. P = ~~P
2. TW(~P) = ~TW(P)
3. PR(~P) = DIS(P)
D. - P / Q - X / Y
1. - ~P / P TOC, INC , PARA
II. Rules of Inference
1. P à Q | -Q à -P TOC , INC , PARA
2. P/Q ó M # P/Q ó P=Q(M) ALL
3. f(a) + a=b à f(b)
4. M # P PROGSYN , DEBUG , PROGAN , DBMSQP , TOC , RECTH , INC , SETH
N # Q
or(M,N) # PvQ
5. M # P(x) PROGSYN , DEBUG , PROGAN , DBMSQP , TOC , RECTH , INC ,
SETH
N # Q(I)*
do(M,N) # P(x) ^ Q(x)
So we use the following methods:
1. X # Y + EQ(I,J)* à X # X RECTH
2. M # P + N # Q à f(M,N) # g(P,Q) PROGSYN
V. Program Synthesis
PROGSYN X # I / YES
Given a value P for input variable I we can work backwards from :
f(M,N) # g(P,Q)
If I = g(P,Q) then X = f(M,N) where M # P and N # Q.
VI. Program Debugging
DEBUG I # J / YES
VII. Program Analysis
PROGAN I # X / YES
VIII. Programming Language Semantics
PLSEM X # Y / YES
Axioms:
MUL(FACTOR,FACTOR,PRODUCT)
EMP(NAME,NUMBER)
"MUL-1" # MUL(I,J,X)* We can multiply
"EMP-1" # (eA)EMP(A,x) List all employee numbers.
"EMP-2" # EMP(X,I) Get an employee's name.
"EMP-3" # EMP(I,X) Get an employee's number.
"EMP-4" # EMP(X,Y) List all employees' name and number.
"s11" # s11(I,J) Substitution is recursive.
"YES-1" # YES(X,Y) YES is r.e.
"YIT-1" # YIY(I,J,K)* YIT is recursive.
Rules:
For any M # P / YES and N # Q / YES we have f(M,N) # g(P,Q), so we add
this to the X # Y / YES.
M # P
N # Q
- - - - -
f(M,N) # g(P,Q)
f(M,N) # g(P,Q)
X # I / YES PROGSYN
f-(X) # g-(I) / YES
IX. Data Base Management System Query Processing
DBMSQP X # I / J
X. Theory of Computation (Turing)
TOC - X / YES
1. CONS: YES , YES ^ ~NO
2. NO / YES
3. ~(YES v NO) / YES
4. NO v ~(YES v NO) / YES OR 2,3
a. NO v ~( (YES ^ ~NO ) v NO ) / YES
b. NO v ~( (YES v NO) ^ (~NO v NO)) / YES
c. NO v ~( (YES v NO) ^ TRUE ) / YES
d. NO v ~( (YES v NO) ) / YES
e. NO v ( ~YES v ~NO ) / YES
f. NO v ~ YES v ~NO / YES
g. ~YES v (NO v ~NO) / YES
h. ~YES v TRUE / YES
i. ~YES / YES
5. ~YES / YES 1 , 4
1. -{ ~(PRvDIS)/PR , DIS/PR , PR = (PR^~DIS) } T1
XI. Recursion Theory (Kleene)
RECTH X # X / YES
s11(I,J)
s11(I,I)
N # s11(I,I)
s11(N,N) # s11(N,N)
M # M
XII. Incompleteness in Logic (Godel)
INC - X / PR
Theorems include:
1. -{ ~P/P }
2. -{ ~PR/PR }
3. -{ ~PR/TW , PR=TW }
4. -{ ~PR/TW , PRàTW , TWàPR } G1IA
5. -{ ~PR/TW , PRàTW , ~PRàDIS } G1IB
6. -{ DIS/TW , TW=~DIS }
7. -{ DIS/TW , TWà~DIS , ~DISàTW }
8. -{ DIS/TW , DIS à ~TW , ~TW à DIS }
9. -{ DIS/TW , PR à TW , TW à PR } S1A
10. -{ DIS/TW , PRàTW , ~PRàDIS } S1B
11. -{ DIS/PR , ~PR=DIS }
12. -{ DIS/PR , ~PRàDIS , DISà~PR } R1
13. -{ -~PR/YES , DIS/YES , ~PRàDIS , DISà~PR } R1 - short
14. -{ ~PR=DIS , DIS/PR }
15. -{ ~(PRvDIS)/PR , DIS/PR , PR = (PR^~DIS) } T1
Bases: P , PR , TW , YES
Known in PA's PR
~PR / TW - TW , PR G1
PR / TW - TW , ~PR
DIS / TW - ~TW , DIS S1
DIS / PR - ~PR , DIS -{ ~PRàDIS , DISà~PR } -{ DEC , CONS } R1
PR / PR
PR / DIS
~TRUE / PR ; PR = (PR ^ ~DIS)
DEC : PR v DIS , TRUE
CONS : ~TRUE / PR
:: ~(PR v DIS) / PR
DIS / PR
~(PR v DIS) v DIS / PR
~PR / PR
In P,|-P,~|-~P PERF
PR = TW
PR à TW
TW à PR
~PR = DIS
~PR à DIS
DIS à ~PR
TW = DIS
TW à DIS
DIS à TW
XIII. Set Theory (ZF)
SETH X / SE
C-B
(more later)
Jan Burse
Chatton's Anti-Razor: "if three things are
not enough to verify an affirmative proposition
about things, a fourth must be added, and so on"
For every "branch" new equations are added.
So there are no visible few first principles
which allow to derive the things under
discussion. Very in contrast to other known
systems.
Also the style of presentation makes it difficult
to follow what the first principles would be.
The style is top down. I.e. some formalism
for a branch, and then plonk some equations or
ways to "solve" things.
Very bad...
Bye
Charlie-Boo wrote:
> ā
> and(M,N) # P ^ Q
> or(M,N) # P v Q
>
> 3. What do we do with the (X,Y) pairs?
>
> What do we want?
>
> a. (I,X) : If I=X then write X I # X / YES PROGANA 3
> b. (X,I) : If I=Y then write Y X # I / YES PROGSYN 1
> c. (I,J) : If I=X and J=Y then write "Yes" I # J / YES DEBUG 2
> d. (X,X) : If X=Y then write X X # X / YES RECTH 7
>
> 4. We solve - X / YES - X / YES TOC 6
>
> a. - ~P/P - ~YES/YES
>
> b. - P / Q , R ā P / Q : - R
> 1. P ā Q | -Q ā -P TOC , INC , PARA
>
> 2. P/Q ó M # P/Q ó P=Q(M) ALL
>
> 3. f(a) + a=b ā f(b)
>
> 4. M # P PROGSYN , DEBUG , PROGAN , DBMSQP , TOC , RECTH , INC , SETH
> N # Q
> or(M,N) # PvQ
>
> 5. M # P(x) PROGSYN , DEBUG , PROGAN , DBMSQP , TOC , RECTH , INC ,
> SETH
> N # Q(I)*
> do(M,N) # P(x) ^ Q(x)
>
> So we use the following methods:
>
> 1. X # Y + EQ(I,J)* ā X # X RECTH
> 2. M # P + N # Q ā f(M,N) # g(P,Q) PROGSYN
> 4. -{ ~PR/TW , PRāTW , TWāPR } G1IA
> 5. -{ ~PR/TW , PRāTW , ~PRāDIS } G1IB
> 6. -{ DIS/TW , TW=~DIS }
> 7. -{ DIS/TW , TWā~DIS , ~DISāTW }
> 8. -{ DIS/TW , DIS ā ~TW , ~TW ā DIS }
> 9. -{ DIS/TW , PR ā TW , TW ā PR } S1A
> 10. -{ DIS/TW , PRāTW , ~PRāDIS } S1B
> 11. -{ DIS/PR , ~PR=DIS }
> 12. -{ DIS/PR , ~PRāDIS , DISā~PR } R1
> 13. -{ -~PR/YES , DIS/YES , ~PRāDIS , DISā~PR } R1 - short
> 14. -{ ~PR=DIS , DIS/PR }
> 15. -{ ~(PRvDIS)/PR , DIS/PR , PR = (PR^~DIS) } T1
>
> Bases: P , PR , TW , YES
>
> Known in PA's PR
> ~PR / TW - TW , PR G1
> PR / TW - TW , ~PR
> DIS / TW - ~TW , DIS S1
> DIS / PR - ~PR , DIS -{ ~PRāDIS , DISā~PR } -{ DEC , CONS } R1
> PR / PR
> PR / DIS
> ~TRUE / PR ; PR = (PR ^ ~DIS)
>
> DEC : PR v DIS , TRUE
> CONS : ~TRUE / PR
> :: ~(PR v DIS) / PR
> DIS / PR
> ~(PR v DIS) v DIS / PR
> ~PR / PR
>
> In P,|-P,~|-~P PERF
> PR = TW
> PR ā TW
> TW ā PR
> ~PR = DIS
> ~PR ā DIS
> DIS ā ~PR
> TW = DIS
> TW ā DIS
> DIS ā TW
Charlie-Boo
> I think CBL system, is a good example of
> Chatton's Anti-Razor: "if three things are
> not enough to verify an affirmative proposition
> about things, a fourth must be added, and so on"
> For every "branch" new equations are added.
No, each branch of Computer Science is different and the equation
defines the branch. That is the first amazing aspect of CBL: We
express all of these various branches in one simple system, CBL.
Note that researchers have yet to realize these connections. For
example, both Marvin Minsky and Hartley Rogers insist that there is no
practical use for the Theory of Computation. However, in CBL we see
that it is almost identical to Program Synthesis, arguably the most
practical branch in all of Computer Science.. The only difference is
an additional axiom of incompleteness -~YES(x,x) in the Theory of
Computation.
> So there are no visible few first principles
CBL and the equations are the first principles. Entire branches of
Computer Science are reduced to simple equations. This instantly
solves many long standing unsolved problems, e.g. Program Synthesis and
the Axiomatization of the Theory of Computation.
> which allow to derive the things under
> discussion. Very in contrast to other known
> systems.
What other system has axiomatized any branch of Computer Science, much
less all ten?
> Also the style of presentation makes it difficult
> to follow what the first principles would be.
> The style is top down. I.e. some formalism
> for a branch, and then plonk some equations or
> ways to "solve" things.
>
> Very bad...
Who else has axiomatized any branch of Computer Science?
C-B
> > à
> > and(M,N) # P ^ Q
> > or(M,N) # P v Q
> >
> > 3. What do we do with the (X,Y) pairs?
> >
> > What do we want?
> >
> > a. (I,X) : If I=X then write X I # X / YES PROGANA 3
> > b. (X,I) : If I=Y then write Y X # I / YES PROGSYN 1
> > c. (I,J) : If I=X and J=Y then write "Yes" I # J / YES DEBUG 2
> > d. (X,X) : If X=Y then write X X # X / YES RECTH 7
> >
> > 4. We solve - X / YES - X / YES TOC 6
> >
> > a. - ~P/P - ~YES/YES
> >
> > b. - P / Q , R à P / Q : - R
> > 1. P à Q | -Q à -P TOC , INC , PARA
> >
> > 2. P/Q ó M # P/Q ó P=Q(M) ALL
> >
> > 3. f(a) + a=b à f(b)
> >
> > 4. M # P PROGSYN , DEBUG , PROGAN , DBMSQP , TOC , RECTH , INC , SETH
> > N # Q
> > or(M,N) # PvQ
> >
> > 5. M # P(x) PROGSYN , DEBUG , PROGAN , DBMSQP , TOC , RECTH , INC ,
> > SETH
> > N # Q(I)*
> > do(M,N) # P(x) ^ Q(x)
> >
> > So we use the following methods:
> >
> > 1. X # Y + EQ(I,J)* à X # X RECTH
> > 2. M # P + N # Q à f(M,N) # g(P,Q) PROGSYN
> > 4. -{ ~PR/TW , PRàTW , TWàPR } G1IA
> > 5. -{ ~PR/TW , PRàTW , ~PRàDIS } G1IB
> > 6. -{ DIS/TW , TW=~DIS }
> > 7. -{ DIS/TW , TWà~DIS , ~DISàTW }
> > 8. -{ DIS/TW , DIS à ~TW , ~TW à DIS }
> > 9. -{ DIS/TW , PR à TW , TW à PR } S1A
> > 10. -{ DIS/TW , PRàTW , ~PRàDIS } S1B
> > 11. -{ DIS/PR , ~PR=DIS }
> > 12. -{ DIS/PR , ~PRàDIS , DISà~PR } R1
> > 13. -{ -~PR/YES , DIS/YES , ~PRàDIS , DISà~PR } R1 - short
> > 14. -{ ~PR=DIS , DIS/PR }
> > 15. -{ ~(PRvDIS)/PR , DIS/PR , PR = (PR^~DIS) } T1
> >
> > Bases: P , PR , TW , YES
> >
> > Known in PA's PR
> > ~PR / TW - TW , PR G1
> > PR / TW - TW , ~PR
> > DIS / TW - ~TW , DIS S1
> > DIS / PR - ~PR , DIS -{ ~PRàDIS , DISà~PR } -{ DEC , CONS } R1
> > PR / PR
> > PR / DIS
> > ~TRUE / PR ; PR = (PR ^ ~DIS)
> >
> > DEC : PR v DIS , TRUE
> > CONS : ~TRUE / PR
> > :: ~(PR v DIS) / PR
> > DIS / PR
> > ~(PR v DIS) v DIS / PR
> > ~PR / PR
> >
> > In P,|-P,~|-~P PERF
> > PR = TW
> > PR à TW
> > TW à PR
> > ~PR = DIS
> > ~PR à DIS
> > DIS à ~PR
> > TW = DIS
> > TW à DIS
> > DIS à TW
Charlie-Boo
> I think CBL system, is a good example of
> Chatton's Anti-Razor: "if three things are
> not enough to verify an affirmative proposition
> about things, a fourth must be added, and so on"
> For every "branch" new equations are added.
> So there are no visible few first principles
> which allow to derive the things under
> discussion. Very in contrast to other known
> systems.
The first problem is to verify and clarify the formalizations of the 10
branches of Computer Science:
logic?
C-B
> > à
> > and(M,N) # P ^ Q
> > or(M,N) # P v Q
> >
> > 3. What do we do with the (X,Y) pairs?
> >
> > What do we want?
> >
> > a. (I,X) : If I=X then write X I # X / YES PROGANA 3
> > b. (X,I) : If I=Y then write Y X # I / YES PROGSYN 1
> > c. (I,J) : If I=X and J=Y then write "Yes" I # J / YES DEBUG 2
> > d. (X,X) : If X=Y then write X X # X / YES RECTH 7
> >
> > 4. We solve - X / YES - X / YES TOC 6
> >
> > a. - ~P/P - ~YES/YES
> >
> > b. - P / Q , R à P / Q : - R
> > 1. P à Q | -Q à -P TOC , INC , PARA
> >
> > 2. P/Q ó M # P/Q ó P=Q(M) ALL
> >
> > 3. f(a) + a=b à f(b)
> >
> > 4. M # P PROGSYN , DEBUG , PROGAN , DBMSQP , TOC , RECTH , INC , SETH
> > N # Q
> > or(M,N) # PvQ
> >
> > 5. M # P(x) PROGSYN , DEBUG , PROGAN , DBMSQP , TOC , RECTH , INC ,
> > SETH
> > N # Q(I)*
> > do(M,N) # P(x) ^ Q(x)
> >
> > So we use the following methods:
> >
> > 1. X # Y + EQ(I,J)* à X # X RECTH
> > 2. M # P + N # Q à f(M,N) # g(P,Q) PROGSYN
> > 4. -{ ~PR/TW , PRàTW , TWàPR } G1IA
> > 5. -{ ~PR/TW , PRàTW , ~PRàDIS } G1IB
> > 6. -{ DIS/TW , TW=~DIS }
> > 7. -{ DIS/TW , TWà~DIS , ~DISàTW }
> > 8. -{ DIS/TW , DIS à ~TW , ~TW à DIS }
> > 9. -{ DIS/TW , PR à TW , TW à PR } S1A
> > 10. -{ DIS/TW , PRàTW , ~PRàDIS } S1B
> > 11. -{ DIS/PR , ~PR=DIS }
> > 12. -{ DIS/PR , ~PRàDIS , DISà~PR } R1
> > 13. -{ -~PR/YES , DIS/YES , ~PRàDIS , DISà~PR } R1 - short
> > 14. -{ ~PR=DIS , DIS/PR }
> > 15. -{ ~(PRvDIS)/PR , DIS/PR , PR = (PR^~DIS) } T1
> >
> > Bases: P , PR , TW , YES
> >
> > Known in PA's PR
> > ~PR / TW - TW , PR G1
> > PR / TW - TW , ~PR
> > DIS / TW - ~TW , DIS S1
> > DIS / PR - ~PR , DIS -{ ~PRàDIS , DISà~PR } -{ DEC , CONS } R1
> > PR / PR
> > PR / DIS
> > ~TRUE / PR ; PR = (PR ^ ~DIS)
> >
> > DEC : PR v DIS , TRUE
> > CONS : ~TRUE / PR
> > :: ~(PR v DIS) / PR
> > DIS / PR
> > ~(PR v DIS) v DIS / PR
> > ~PR / PR
> >
> > In P,|-P,~|-~P PERF
> > PR = TW
> > PR à TW
> > TW à PR
> > ~PR = DIS
> > ~PR à DIS
> > DIS à ~PR
> > TW = DIS
> > TW à DIS
> > DIS à TW
Peter_Smith
Charlie-Boo wrote:
4. "If an axiomatizable system is consistent and decidable, then its
refutable sentences coincide with its unprovable sentences, but the
former is recursively enumerable while the latter is not."
Really?? Take the theory which is built in a propositional language
with P, Q the only atoms, and the usual connectives, and whose sole
axiom is P.
This theory is (i) consistent, (ii) decidable [since X will be a
theorem just if P --> X is a tautology], but (iii) the sentence Q is
evidently unprovable but not refutable. So it is NOT the case that if
an axiomatizable system is consistent and decidable, then its refutable
sentences coincide with its unprovable sentences.
Charlie-Boo
> Charlie-Boo wrote:
> > 4. "If an axiomatizable system is consistent and decidable, then its
> > refutable sentences coincide with its unprovable sentences, but the
> > former is recursively enumerable while the latter is not."
>
> "coincide", then, OBVIOUSLY, since they are THE SAME collection
> of sentences,
Hi,
That's just a synonym, not a conclusion.
> if ONE is r.e, then the other, must also be r.e.
Therefore no system is consistent and decidable. qed
> More to the point,
> if the system is decidable, then BY DEFINITION (REGARDLESS of
> whether it is consistent OR NOT), its provable sentences are just
> exactly the denials of its refutable ones,
So? You're confused if you think that relates to my proof. I equate
the provable sentences with the unrefutable sentences, not the denials
of the refutable sentences.
C-B
> and EVERY sentence in the
> language is one or the other, and BOTH classes are recursively
> enumerable.
> BY DEFINITION.
> Implying that you don't know the definitions of the terms you are
> using.
>
> Can't you just go back to school for a year and get grounding in the
> basic concepts before presuming to pontificate further?
Charlie-Boo
Peter_Smith wrote:
> Charlie-Boo wrote:
> 4. "If an axiomatizable system is consistent and decidable, then its
> refutable sentences coincide with its unprovable sentences, but the
> former is recursively enumerable while the latter is not."
>
> Really?? Take the theory which is built in a propositional language
> with P, Q the only atoms, and the usual connectives, and whose sole
> axiom is P.
>
> This theory is (i) consistent, (ii)
The assertion that your system "is decidable but the sentence Q is
unprovable but not refutable" is inconsistent.
> So it is NOT the case that if
> an axiomatizable system is consistent and decidable, then its refutable
> sentences coincide with its unprovable sentences.
It is simple propositional calculus.
C-B
Chip Eastham
Charlie, you are either using very non-standard terminology (in which
case you need to define your terms more fully) or you are simply
mistaken.
Consider the formal first-order theory, predicate calculus with
equality and one "extra-logical" axiom:
for all x,y ( x = y )
This theory has a canonical model with the standard interpretation
of equality, and hence is consistent and complete (therefore
decidable).
You need a great deal more than "simple propositional calculus"
to get to an incompleteness result ala Goedel or Turing.
regards, chip
george
Peter_Smith wrote:
> Charlie-Boo wrote:
> 4. "If an axiomatizable system is consistent and decidable, then its
> refutable sentences coincide with its unprovable sentences, but the
> former is recursively enumerable while the latter is not."
>
> Really??
> Take the theory
There is going to be a tragic disconnect here between
"undecidable theory" and "undecidable system".
Normally this is NOT supposed to be important;
the PURPOSE of the system is to produce the theory.
> which is built in a propositional language
> with P, Q the only atoms, and the usual connectives, and whose sole
> axiom is P.
This theory is trivially incomplete.
It cannot decide Q.
>
> This theory is (i) consistent,
Right.
> (ii) decidable [since X will be a theorem just if P --> X is a tautology],
This is a finite 0th-order theory; it is trivially decidable.
But it doesn't decide Q.
> but (iii) the sentence Q is
> evidently unprovable but not refutable. So it is NOT the case that if
> an axiomatizable system is consistent and decidable, then its refutable
> sentences coincide with its unprovable sentences.
What you mean by decidable here is not what I think *he* meant.
george
> > More to the point,
> > if the system is decidable,
This is ambiguous; smarter people than I are interpreting
it to mean that you can decide whether something is or isn't
provable, not that the theory decides every question.
> > then BY DEFINITION (REGARDLESS of
> > whether it is consistent OR NOT), its provable sentences are just
> > exactly the denials of its refutable ones,
> So? You're confused if you think that relates to my proof.
Sorry, you're the one who is confused.
> I equate
> the provable sentences with the unrefutable sentences,
You CAN'T do that. For systems rich enough to satisfy the hypotheses
of Godel's theorem, the unrefutable sentences CAN'T all be provable.
Indeed, for any incomplete system, the unrefutable sentences CAN'T all
be provable.
As Peter Smith already told you, if you can somehow get Q into the
system despite its not being mentioned in an axiom (because the only
axiom is P), then both Q and ~Q are unrefutable (since neither of them
is provable), but obviously neither of them is provable.
One way to make sure Q is mentionable is to have 2 axioms specifying
the theory:
P v Q and
P v ~Q
Here, you can clearly decide that both Q and ~Q are not theorems.
But you cannot decide Q.
george
Chip Eastham wrote:
> You need a great deal more than "simple propositional calculus"
> to get to an incompleteness result ala Goedel or Turing.
But as Peter Smith has already told you, DON'T need more than
that just to get a theory that is incomplete in the sense of Godel's
1st Incompleteness theorem, "negation" incomplete;
e.g., the empty theory is incomplete, or the propositional theory with
the sole axiom P is incomplete, or the theory propositional theory
with the 2 axioms
P v Q and
P v ~Q is incomplete (it doesn't decide Q).
One problem with berating people for non-standard terminology
is that the standard terminology is so eminently worthy of being
berated. Godel really should've had better sense than to bequeath
us BOTH a completeness theorem AND and incompleteness theorem
for the SAME logic.
Chip Eastham
I tried to reply a couple of times before and got errors,
so apologies if on some servers this appears again.
The results of Goedel and Turing are for essentially
incomplete theories. Such a thing is impossible with
the propositional calculus alone. Any consistent
theory in the propositional calculus may be extended
to a complete, consistent theory on the same
sentential letters. In your example, either P and Q
as axioms, or P and ~Q, will suffice.
Raising the terminology isse was a request to
Charlie to define his terms, not for the sake of
berating his usage, but in hope of understanding.
The example I gave was intended to illustrate the
standard meaning of decidable and consistent.
Perhaps there is simply an omitted hypothesis
in his original post.
There are various completeness theorems for logics,
and Goedel's doctoral dissertation proves the one
for predicate calculus (1929, published 1930). His
incompleteness theorems (first and second) are
with regard to a slight extension of Peano arithmetic,
and what is significant as pointed out above is the
notion of essential incompleteness, ie. that no
formal first-order extension of Peano arithmetic can
be both consistent and complete. However if PA
is consistent, a complete extension exists but is
not "formal" because no recursive set of such
axioms is possible.
regards, chip
Charlie-Boo
> > > 4. "If an axiomatizable system is consistent and decidable, then its
> > > refutable sentences coincide with its unprovable sentences, but the
> > > former is recursively enumerable while the latter is not."
> Charlie, you are either using very non-standard terminology (in which
> case you need to define your terms more fully) or you are simply
> mistaken.
Oops. My bad. Change "decidable" to "all sentences are
decidable" (or simply "complete.")
Unfortunately, common usage is that decidable applied to a system does
not mean the same thing as decidable applied to a sentence being true
of all sentences in the system. (I have read at least 3 texts that
apologize for the inconsistency. In my own studies I use decidable
system to mean that all sentences in the system are provable or
refutable. I neglected to substitute more common terminology when I
cut and pasted it in response to questions about CBL.) Now it
faithfully represents Rosser's conclusion (the system is not both
consistent and complete.) Thanks for noticing.
Now does it prove Rosser 1936, and who else has shown such a short,
simple proof? (Not to mention that it is formally generated.)
> Consider the formal first-order theory, predicate calculus with
> equality and one "extra-logical" axiom:
>
> for all x,y ( x = y )
>
> This theory has a canonical model with the standard interpretation
> of equality, and hence is consistent and complete (therefore
> decidable).
>
> You need a great deal more than "simple propositional calculus"
> to get to an incompleteness result ala Goedel or Turing.
The above proof of Rosser 1936 uses only Propositional Calculus applied
to definitions and Theory of Computation results (the latter being
producable from CBL rules which are also quite simple.)
C-B
> regards, chip