Search All of the Math Forum:
Views expressed in these public forums are not endorsed by
NCTM or The Math Forum.


Math Forum
»
Discussions
»
sci.math.*
»
sci.math
Notice: We are no longer accepting new posts, but the forums will continue to be readable.
Topic:
logical inference
Replies:
1
Last Post:
Nov 16, 2012 7:48 PM




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 secondorder sentence is universally valid, i.e., true in all domains under standard semantics.
(Completeness) Every universally valid secondorder formula, under standard semantics, is provable.
(Effectiveness) There is a proofchecking 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!



