/* Copyright (c) 2010,2014 Dennis J. Darland */
/* Prolog predicates to simulate Dennis J. Darlands philosophy. */
/* Written 6/14/2007 */
/* Revised 12/26/2009 - adding perception */
/* Revised 1/14/2010 - after perception breakthrough thoughts */
/* Revised again 1/16/2010 - after more perception breakthrough thoughts */
/* Reviswd again 7/31/2010 - after more general thoughts on philosophy of mind*/
/* Reviswd again 10/13/2010 - continued more general thoughts on philosophy of mind*/
/* Reviswd again 10/13/2014 - Revising for a mistake and for purpose of answering Sitch's examples case by case */
/* myphil.pl */
/* to run in swi-prolog under cygwin:
   pl
  consult('someexample.pl').
  consult('myphil0002.pl').
  protocol('someoutput.txt').
 ... test queries
  noprotocol.
*/
/* ----------------------------------------------------------
7/31/2010 More Ideas on philosophy of mind added
10/13/2010 Revised Further
10/14/2010 Revised Further
------------------------------------------------------*/

common_symbol1(Subject1,Subject2,Aword,A,Time) :-
	external_symbol1(Subject1,Aword,A1,Time),
	external_symbol1(Subject2,Aword,A2,Time),
	symbol1(Subject1,A1,A,Time),
	symbol1(Subject2,A2,A,Time).

/* Above Subject1 and Subject2 are two persons (which are complex)
   
external_symbol1 is a predicate which may be true at some Time when the external
(written or spoken word Aword of type 1 is associated with a internal symbol
A1 or A2 for Subject 1 or subject2 respectively.)
   
symbol1 is a predicate which may be true at timw Time when the internal symbol
A1 or A2 is associated with the object (property A). */
   
	
common_symbol0(Subject1,Subject2,Aword,A,Time) :-
	external_symbol0(Subject1,Aword,A1,Time),
	external_symbol0(Subject2,Aword,A2,Time),
	symbol0(Subject1,A1,A,Time),
	symbol0(Subject2,A2,A,Time).
	
/* external_symbol0 is a predicate which may be true at some Time when the external
(written or spoken word Aword of type 0 is associated with a internal symbol
A1 or A2 for Subject 1 or subject2 respectively.)
   
symbol0 is a predicate which may be true at timw Time when the internal symbol
A1 or A2 is associated with the object (thing A). */
   

recognizes_perception(Subject,PR,PA,Time) :-
	perceives(Subject, Time, PR, PA) :- 
	symbol1(Subject,PR,R,Time),
	symbol0(Subject,PA,A,Time).

/* ------------------------------------------------------------------------
1/23/2010 ideas on perception  
Subject = person doing perceiving
Time = time of perceiving 
Sense_data = particular (but complex) entity = a complete set of a persons
    experiences at that time 
Sd_obj_a =  piece of a Sense_data corresponding to an object (e.g. circular part) 
[could also be additional Sd_obj_b, Sd_obj_c, ...
Sd_pred = predicate true of a Sd_obj (e.g. red)
PA = predicate describing an external object that ordinarily would cause 
    such experience of external object A
PR = predicate corresponding to predicate R of external object that ordinarily
    would cause such experience of object A having such predicate R
A = object perceived
could also be a B, C, ...
R = prredicate object perceived as having (property)  
------------------------------------------------------------------------*/

perceives(Subject, Time, PR, PA) :- 
    experiences(Subject, Time, Sense_Data), 
    phys_pred(R),
    phys_obj(A),
    normal_pred_conditions(PR, R),
    normal_obj_conditions(PA, A),
    apply(PR,[PA]),
    perceptual_obj_relation(Sd_obj_a, PA),
    perceptual_pred_relation(Sd_pred, PR),
    sub_sd_object(Sense_data, Sd_obj_a),
    apply(Sd_pred, [Sd_obj_a]).

hallucinates(Subject, Time, PR, PA) :- 
    experiences(Subject, Time, Sense_Data), 
    phys_pred(R),
    phys_obj(A),
    normal_pred_conditions(PR, R),
    normal_obj_conditions(PA, A),
    not(apply(PR,[PA])),
    perceptual_obj_relation(Sd_obj_a, PA),
    perceptual_pred_relation(Sd_pred, PR),
    sub_sd_object(Sense_data, Sd_obj_a),
    apply(Sd_pred, [Sd_obj_a]).

hallucinates(Subject, Time, PR, PA) :- 
    experiences(Subject, Time, Sense_Data), 
    phys_pred(R),
    phys_obj(A),
    not(normal_pred_conditions(PR, R)),
    perceptual_obj_relation(Sd_obj_a, PA),
    perceptual_pred_relation(Sd_pred, PR),
    sub_sd_object(Sense_data, Sd_obj_a),
    apply(Sd_pred, [Sd_obj_a]). 

hallucinates(Subject, Time, PR, PA) :- 
    experiences(Subject, Time, Sense_Data), 
    phys_pred(R),
    phys_obj(A),
    not(normal_obj_conditions(PA, A)),
    perceptual_obj_relation(Sd_obj_a, PA),
    perceptual_pred_relation(Sd_pred, PR),
    sub_sd_object(Sense_data, Sd_obj_a),
    apply(Sd_pred, [Sd_obj_a]). 

/*--------------------------------------------------------------
EXAMPLE 1
Tom and Harry see same red circle

VARIABLE            Tom              Harry
Subject             tom              harry
Time                1:00pm           1:00pm
Sense_data          toms_sense_data  harrys_sense_data
Sd_obj_a            toms_sns_circle  harrys_sns_circle
Sd_pred             toms_sns_red     harrys_sns_red
PA                  circlularity     circlularity
PR                  red              red
A                   circular_object  circular_object
R                   redness          redness (not sure need both PR & R)

in this case all relations in "perceived" above would hold for these arguments
-------------------------------------------------------------------------
EXAMPLE 2
Tom hallucinates red circle and Harry sees red circle

VARIABLE            Tom              Harry
Subject             tom              harry
Time                1:00pm           1:00pm
Sense_data          toms_sense_data  harrys_sense_data
Sd_obj_a            toms_sns_circle  harrys_sns_circle
Sd_pred             toms_sns_red     harrys_sns_red
PA                  circlularity     circlularity
PR                  red              red
A                   circular_object  circular_object
R                   redness          redness (not sure need both PR & R)

for tom either 
    apply(PR,[PA]) 
or 
    normal_pred_conditions(PR, R),
or
    normal_obj_conditions(PA, A).
would fail
------------------------------------------------------------------*/
/* 5/1/2014 - belief_r eliminated - now just have belief */

understand(S,R,A,T) :-  symbol1_r(S,W,R,T) ,symbol0_r(S,X,A,T).

understand(S,R,A,B,T) :-  symbol1_r(S,W,R,T) ,symbol0_r(S,X,A,T) ,symbol0_r(S,Y,B,T).

understand(S,R,A,B,C,T) :-  symbol1_r(S,W,R,T) ,symbol0_r(S,X,A,T) ,symbol0_r(S,Y,B,T),symbol0_r(S,Z,C,T).

logical_form(RF,W,X,Y) :- RF == 'r(a,b)', symbol1_r(S,W,R,T), symbol0_r(S,X,A,T), symbol0_r(S,Y,B,T).

proposition(R,A) :- understand(S,R,A,T). 
proposition(R,A,B) :- understand(S,R,A,B,T). 
proposition(R,A,B,C) :- understand(S,R,A,B,C,T). 

true_proposition(R,A,T) :- proposition(R,A) , apply(R,[A,T]).
true_proposition(R,A,B,T) :- proposition(R,A,B) , apply(R,[A,B,T]).
true_proposition(R,A,B,C,T) :- proposition(R,A,B,C) , apply(R,[A,B,C,T]).
/* T1 is time of belief T2 is time it is believed to be true */
true_belief(S,R,A,T1,T2) :- belief(S,R,A,T1) , apply(R,[A,T2]).
true_belief(S,R,A,B,T1,T2) :- belief(S,R,A,B,T1) , apply(R,[A,B,T2]).
true_belief(S,R,A,B,C,T1,T2) :- belief(S,R,A,B,C,T1) , apply(R,[A,B,C,T2]).

symbol0(X) :- symbol0_r(S,X,A,T).

symbol1(X) :- symbol1_r(S,X,A,T).

/* I THINK I SHOULD GET RID OF name_1 */
name_1(W) :- belief_r(S,W,X,T).

/* the _1 is just to distinguish it from the built in 'name' */
/* I THINK I SHOULD GET RID OF name_1 

name_1(X) :- belief_r(S,W,X,T).

name_1(W) :- belief_r(S,W,X,Y,T).

name_1(X) :- belief_r(S,W,X,Y,T).

name_1(Y) :- belief_r(S,W,X,Y,T).

name_1(W) :- belief_r(S,W,X,Y,Z,T).

name_1(X) :- belief_r(S,W,X,Y,Z,T).

name_1(Y) :- belief_r(S,W,X,Y,Z,T).

name_1(Z) :- belief_r(S,W,X,Y,Z,T).
*/


/* get intensional predicate to test extensionality of classes */
tom_believes_now(P_N,X_N) :- symbol1_r(tom,P_N,P,now), symbol0_r(tom,X_N,X,now), belief(tom,P_N,X_N,now).

/* Principia Mathematica definition of classes in Prolog */
/* THIS ONE TO BE USED WITH RUSSELLS CLASS added args to distinguish */
true_of_class('RUSSELL','RUSSELL',F_N,PSI_N) :-  symbol1_r(S,F_N,F,T), symbol1_r(S,PSI_N,PSI,T), symbol1_r(S,PHI_N,PHI,T), equiv_r(PSI,PHI),  writeln(['applying(russels class) ',F_N,' to ',PHI_N, ' and ',PHI_N]), apply(F,[PHI_N,PHI_N]).


/* THIS ONE WORKS WITH member_of, and any other 'class function' with 2 args */
true_of_class(F_N,PSI_N,X_N) :-  symbol1_r(S,F_N,F,T), symbol1_r(S,PSI_N,PSI,T),symbol0_r(S,X_N,X,T), predicative(PHI_N,PHI), equiv_r(PSI,PHI) ,apply(F,[PHI_N,X_N]), X_N \= no.

/* for 'class functions' with 1 arg */ 
true_of_class(F_N,PSI_N) :- symbol1_r(S,F_N,F,T), symbol1_r(S,PSI_N,PSI,T), symbol1_r(S,PHI_N,PHI,T), equiv_r(PSI,PHI),  apply(F,[PHI_N]).


equiv_r(not_member_of_self,not_member_of_self). /* otherwise run out of stack */equiv_r(true_of_class,true_of_class). /* otherwise run out of stack */
equiv_r(member_of,member_of). /* otherwise run out of stack */
equiv_r(PSI,PHI) :- not(not_equiv(PSI,PHI)).
not_equiv(PSI,PHI) :- apply(PSI,[X]),not(apply(PHI,[X])).
not_equiv(PSI,PHI) :- apply(PHI,[X]), not(apply(PSI,[X])).
not_equiv(PSI,PHI) :- apply(PSI,[X,Y]),not(apply(PHI,[X,Y])).
not_equiv(PSI,PHI) :- apply(PHI,[X,Y]), not(apply(PSI,[X,Y])).
not_equiv(PSI,PHI) :- apply(PSI,[X,Y,Z]),not(apply(PHI,[X,Y,Z])).
not_equiv(PSI,PHI) :- apply(PHI,[X,Y,Z]), not(apply(PSI,[X,Y,Z])).
not_equiv(PSI,PHI) :- apply(PSI,[W,X,Y,Z]),not(apply(PHI,[W,X,Y,Z])).
not_equiv(PSI,PHI) :- apply(PHI,[W,X,Y,Z]), not(apply(PSI,[W,X,Y,Z])).
member_of(PHI_N,X_N) :- symbol1_r(S,PHI_N,PHI,T), apply(PHI,[X]).


/* RUSSELLs PARADOX */
not_member_of_self(X,X_N) :- symbol1_r(S,X_N,X,T), true_of_class('RUSSELL','not_member_of_self','not_member_of_self'). 
not_member_of_self(X,X_N) :- symbol1_r(S,X_N,X,T), not(true_of_class('member_of','not_member_of_self','not_member_of_self')). 
russells_class :- true_of_class('RUSSELL',X,Y).

intensional(R) :- symbol1_r(S,R_N,R,T),symbol1_r(S,X_N,X,T),symbol1_r(S,Y_N,Y,T),symbol0_r(S,A_N,A,T), apply(R,[X,A]) , equiv_r(X,Y), not(apply(R,[Y,A])), A \= no.

intensional(R) :- symbol1_r(S,F_N,F,T), symbol1_r(S,R_N,R,T),symbol1_r(S,X_N,X,T),symbol1_r(S,Y_N,Y,T),symbol0_r(S,A_N,A,T),symbol0_r(S,B_N,B,T), apply(R,[F,X,A,B]) , equiv_r(X,Y),not(apply(R,[F,Y,A,B])), A \= no.
intensional(R) :- symbol1_r(S,R_N,R,T),symbol1_r(S,X_N,X,T),symbol1_r(S,Y_N,Y,T),symbol0_r(S,A_N,A,T), apply(R,[S,X_N,A_N,T]) , equiv_r(X,Y),not(apply(R,[S,Y_N,A_N,T])), A \= no.
/* WITH DEBUGGING 
intensional(R) :- symbol1_r(S,F_N,F,T), symbol1_r(S,R_N,R,T),symbol1_r(S,X_N,X,T),symbol1_r(S,Y_N,Y,T),symbol0_r(S,A_N,A,T),symbol0_r(S,B_N,B,T), writeln(['intensionsal R = ',R,' F = ',F,' A = ',A,' B = ',B]),apply(R,[F,X,A,B]) , equiv_r(X,Y),not(apply(R,[F,Y,A,B])).
intensional(R) :- symbol1_r(S,F_N,F,T), symbol1_r(S,R_N,R,T),symbol1_r(S,X_N,X,T),symbol1_r(S,Y_N,Y,T),symbol0_r(S,A_N,A,T), writeln(['intensionsal R = ',R,' F = ',F,' A = ',A,' T = ',T ]),apply(R,[F,X,A,T]) , equiv_r(X,Y),not(apply(R,[F,Y,A,T])), A \= no.
*/
intensional(R) :- symbol1_r(S,F_N,F,T), symbol1_r(S,R_N,R,T),symbol0_r(S,X_N,X,T),symbol1_r(S,Y_N,Y,T),symbol0_r(S,A_N,A,T),symbol0_r(S,B_N,B,T),symbol0_r(S,C_N,C,T),apply(R,[F,X,A,B,C]) ,equiv_r(X,Y), not(apply(R,[F,Y,A,B,C])), A \= no.

intensional(R) :- symbol1_r(S,R_N,R,T),symbol0_r(S,X_N,X,T),symbol1_r(S,Y_N,Y,T),symbol0_r(S,A_N,A,T),symbol0_r(S,B_N,B,T),apply(R,[S,X,A,B,T]) ,equiv_r(X,Y), not(apply(R,[S,Y,A,B,T])) , A \= no.

/* NOT NEEDED YET
intensional(R) :- symbol1_r(S,F_N,F,T), symbol1_r(S,R_N,R,T),symbol0_r(S,X_N,X,T),symbol0_r(S,A_N,A,T),symbol0_r(S,B_N,B,T),symbol0_r(S,C_N,C,T),symbol0_r(S,D_N,D,T),apply(R,[F,X,A,B,C,D]) ,equiv_r(X,Y), not(apply(R,[F,Y,A,B,C,D])).
*/

extensional(R) :- symbol1_r(S,R_N,R,T) ,not(intensional(R)).