Drexel dragonThe Math ForumDonate to the Math Forum



Search All of the Math Forum:

Views expressed in these public forums are not endorsed by Drexel University or The Math Forum.


Math Forum » Discussions » sci.math.* » sci.math.independent

Topic: logical inference
Replies: 1   Last Post: Nov 16, 2012 7:48 PM

Advanced Search

Back to Topic List Back to Topic List Jump to Tree View Jump to Tree View  
Graham Cooper

Posts: 4,227
Registered: 5/20/10
Re: logical inference
Posted: Nov 16, 2012 7:48 PM
  Click to see the message monospaced in plain text Plain Text   Click to reply to this topic Reply

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!




Point your RSS reader here for a feed of the latest messages in this topic.

[Privacy Policy] [Terms of Use]

© Drexel University 1994-2014. All Rights Reserved.
The Math Forum is a research and educational enterprise of the Drexel University School of Education.