Search All of the Math Forum:
Views expressed in these public forums are not endorsed by
Drexel University or The Math Forum.
|
|
|
|
Re: logical inference
Posted:
Nov 16, 2012 7:48 PM
|
|
On Nov 17, 2:43 am, Frederick Williams <freddywilli...@btinternet.com>
wrote:
> RichD wrote:
>
> > I saw on another board, someone said that the rules of inference for
> > second order logic are unknown, actually undecidable. Which means
> > we have no way to check proofs?
>
> > Can anyone explain or expand on this?
>
> You may wish to read
> https://en.wikipedia.org/wiki/Second_order_logic#Metalogical_results.
>
That's exactly what I said!
Metalogical results
It is a corollary of Gödel's incompleteness theorem that there is
no
deductive system (that is, no notion of provability) for second-
order
formulas that simultaneously satisfies these three desired
attributes
(Soundness) Every provable second-order sentence is universally
valid, i.e., true in all domains under standard semantics.
(Completeness) Every universally valid second-order formula, under
standard semantics, is provable.
(Effectiveness) There is a proof-checking algorithm that can
correctly
decide whether a given sequence of symbols is a valid proof or not.
[HERC]
In that case proofs about 2OL formula would tend to be consistency
and closure proofs, so I imagine Godel's Statement is the reason for
what you heard.
I just prefaced it with a warning that ZUHAIR et al. call 2OL
ranging over uncountable sets
============================================
FINE I'll take all my new Logic Technology elsewhere if that's the
treatment I get for advancing the field..
I MADE 3 MAJOR ADVANCEMENTS THIS WEEK WITH AUTOMATED FORMAL SYSTEMS
1/ ENCODING A(X) as a subset predicate { x | D(x) } C { x |
P(x) }
2/ ITERATIVE BACKTRACKING SOLVER that will work with 1 SQL JOIN QUERY
to do all the predicate matching.
vert ( pnt( 1,2 ) pnt( 1,4 ) )
This will be
ID REF FIELD TYP
=================
1 11 vert H
1 12 pnt P
1 13 pnt P
1 121 1 T
1 122 2 T
1 131 1 T
1 132 4 T
vert ( pnt( X,Y ) pnt( X,Z ) )
ID REF FIELD TYP
=================
21 11 vert H
21 12 pnt P
21 13 pnt P
21 121 X V
21 122 Y V
21 131 X V
21 132 Z V
Something like
SELECT * FROM TTAILS, TPRO
WHERE TTAILS.REF = TPRO.REF
AND TTAILS.FIELD = TPRO.FIELD
GROUP BY ID
ORDER BY ID DESCENDING
This performs 5 pages of coding for UNIFY(f1, f2) in 5 lines of SQL!
Butt... since ACTUAL WORKING FORMAL SYSTEMS written in predicates
isn't your thing...
I'll take my new information technology elsewhere.
www.microPROLOG.com
Bye! YOU MORONS & LOSERS!
|
|
|
|
