Claus-Peter Wirth's Scientific Convictions

• Unwürdig eines wissenschaftlich sein wollenden Denkers aber ist es, wenn er den hypothetischen Ursprung seiner Sätze vergisst. Der Hochmuth und die Leidenschaftlichkeit, mit der solche versteckte Hypothesen vertheidigt werden, sind die gewöhnlichen Folgen des unbefriedigenden Gefühls, welches ihr Vertheidiger in den verborgenen Tiefen seines Gewissens über die Berechtigung seiner Sache hegt. (Rede "Die Thatsachen in der Wahrnehmung" von Hermann von Helmholtz, gehalten zur Stiftungsfeier der Friedrich Wilhelms-Universität zu Berlin am 3. August 1878. Seite 36, Verlag von August Hirschwald, Berlin, 1879)
• The task of the scientist, however, is no longer `to search for the truth', or `to praise god', or `to systematize observations', or `to improve predictions'. These are but side effects of an activity to which his attention is now mainly directed and which is `to make the weaker case the stronger' as the sophists said, and therby to sustain the motion of the whole. (Paul Feyerabend, Against Method, 1975)
• One shows the completeness of a calculus to know that it cannot be too useful in practice. (Peter Baumgartner, 1998)
• Everything CP says on logic is always right. (Chad E. Brown, 2004)
• Everytime CP says something, it is so strange that you have to check it out, but at the end it is always true. (Martin Homik, 2005)
• What Hilbert and still Hintikka never understood was that the Axiom of Choice is not on the possible existence of choice functions but on their citizenship in the state of set theory. (Robert B., 1999)
• If the excellent book of Peter Aczel on possibly non-wellfounded sets finds enough readers, his improved set theory will be as beneficial for the 21. century as Cantor's work was for the 20. (Robert B., 1999)
• Specifications should express only what is important for the specifier. A proper semantics for such partial specifications must be based on a class of different models instead of a single one. A free or initial model can serve for a minimal implementation but is not adequate for defining the semantics of partial specifications. Similarly, specification in Z is no specification but paradigmatic implementation. Just like {{}} is not the meaning of the number 1 but its standard implementation in set theory. (Robert B., 1999)
• Jaakko Hintikka's IF logic is like French in that certain parts of a sentence disappear on negation. E.g. the Henkin quantified sentence (Ax)(Eu)(Ay)(Ev/x)S negates to (Ex)(Au)(Ey)(Av)not(S). Note that the /x disappeared. This is like the pronunciation of the consonant t in: Il est allemand. Il n'est pas allemand. Note that even if we keep the /x in the style of Wilfrid Hodges, the /x has no effect on the truth of the formula anymore, while it was crucial before negation. This is really confusing to me. I never was able to learn French properly for the same reason. (CP, 2002)
• In his great book "First-Order Logic and Automated Theorem Proving", Fitting (1996) attributes alpha, beta, gamma, delta primarily to formulas (instead of rules as seems to be Smullyan's intention). This may be well justified for pedagogical reasons, but as this book is now so much of a standard, I consider this to be problematic. Note that Fitting (1996) gets branching alpha rules on p. 51, whereas in Smullyan (1968) the beta stands for the b of branching. In different words: If we attribute alpha, beta etc. to rules, the meaning survives a duality-switch from positive to refutational theorem proving, which is not the case when Fitting attributes them to formulas, whereby he produces just the same confusion which made the notion of "weak" and "strong" quantifiers nearly disappear. (CP, 2002)
• Functions are nothing but (right-) unique relations. (CP, 1998)

  • car(cons(x,y))=x; 
    cdr(cons(x,y))=y.
    

    is semantically just like (in different language!)

    CAR(cons(x,y),x); 
    CDR(cons(x,y),y).
    

    and does not imply

    car(nil)=\bot
    

    since

    CAR(nil,\bot)
    

    is not implied.
  • "f o g" means "g" after "f" not concerning whether "f" and "g" are only relations or even functions.
• The notion of a "constructor symbol" must be based on the signature only, not on the axioms of a specification. (CP, 1998)
• A (possibly partial) characteristic function defined via conditional equations is better than a PROLOG-like defined predicate because it works well in all data models, while the predicate needs an initial or a free model. For example, for l denoting finite lists

  head(cons(x,l)) = x
  tail(cons(x,l)) = l
  null(nil)       = true
  null(cons(x,l)) = false
  memberp(x,l) = true  <-- null(l) = false, head(l) = x
  memberp(x,l) = true  <-- null(l) = false, memberp(x,tail(l)) = true 
  memberp(x,l) = false <-- null(l) = true
  

  is better than

  head(cons(x,l)) = x
  tail(cons(x,l)) = l
  NULL(nil)
  NOTNULL(cons(x,l))
  MEMBER(x,l) <-- NOTNULL(l), MEMBER(x,tail(l))
  MEMBER(x,l) <-- NOTNULL(l), head(l) = x
  

  For infinite streams l, however, we need the free model also for the version with the characteristic functions when we want to guarantee that, for an infinite list l in that x does not occur, memberp(x,l) to is unequal to true. (CP, 1998)
• It does not seem to be completely superfluous to note that the better specification of the previous item is not good. The following versions are getting better: Firstly, there is a version with less function symbols:

  memberp(x,cons(y,l)) = true <-- y = x
  memberp(x,cons(y,l)) = true <-- memberp(x,l) = true 
  memberp(x,nil      ) = false 
  

  Secondly, there is a version which is inductively equivalent but deductively stronger:

  or(true ,y    ) = true
  or(false,y    ) = y
  or(x    ,true ) = true
  or(x    ,false) = x
  eq(x,y) = true  <-- x = y
  eq(x,y) = false <-- x=/=y
  memberp(x,cons(y,l)) = or(memberp(x,l),eq(y,x))
  memberp(x,nil      ) = false 
  

  Finally, there is a version that combines both advantages:

  memberp(x,cons(y,l)) = true         <-- y = x
  memberp(x,cons(y,l)) = memberp(x,l) <-- y=/=x
  memberp(x,nil      ) = false 
  

  This last version is really the best. It has the same deductive strength as the second. It has the same number of function symbols as the first. Moreover it provides the easiest unfolding via a complete case analysis (first syntactically, second semantically on y=x). (CP, 2005)