Logic is about reasoning that is guaranteed to go from true
statements to true statements. In other words, it is about eliminating
forms of reasoning that lead you astray. The study of this kind of
reasoning has some important results.
A software developer can choose to be logical in several ways. Thus a programmer (if any good at all) has to work within the formal language of a programming language. Many programming ideas come from the symbolic logics that started up when George Boole worked on "The Laws of Thought". Better programmers have the abillity to reason out what their programs will do. They may do this with a speed that looks like intuition, and may be loath to express how they do it however. Most can give a very logical account of the behavior of their programs if they have the time to do so. In some fields (published algorithms, safety critical projects, etc) programs have even proved to satisfy their specifications.
However at this level of skill the software developer needs a very clear definition of how the software behaves. Logics can be used to write these specifications - but they are not cheap. However just because a program meets a specification this does not mean that the client is satisfied. To be more sure of this one needs to know what the client wanted -- not as a piece of software -- but as an improved "real world". These requirements express wishes. Indeed one way to get them is to ask a user "If you had a magic wand what would it do for you?". Finally (according to Michael A Jackson) you can only show that a specification (of the software) satisfies the user (requirements) by using domain knowledge -- facts about the real world.
The good news is that software developers only need the simplest forms of logic and algebra. The calculus is not very useful in most domains.
A logician has to work with the smallest system that models the thinking that the logician is interested in. The engineer needs more than the minimum. Therefore what a logician sees and presents as a result in a logical system is taken as a given assumption or rule by the engineer. A workable logic therefore needs a comparatively rich set of assumptions and notation with more than the usual amount of redundancy. This is how the logic of MATHS is presented in these manuals.
However the Euclid's approach - assume a small set of independent axioms and deduce many results is good teaching and learning. It provides training in reasoning. It provides a structure for the teacher. It reduces the mnemonic load and also provides a mnemonic structure. It also provides a normal form for newly created models. After mastering this system however an engineer will tend to take it all for granted.
For an alternative approach to teaching the use of logic as a tool see [ logicthetool.html ]
For an informal and general introduction to my approach to logic see [ intro_README.html ] and [ intro_logic.html ]
Links to Detailed Theory
It is assumed that each 'Type' follows a common generic set of formal
rules. To avoid paradoxes we do not define 'Type' here. Informally we can
define a "Type" to be a collection of objects to which LPC with equality
applies. We will use identifiers starting with a capital T to indicate typical
types. Later we will use "Sets" as another a generic Type.
Properties of several objects at one time: the sum of x and y is z,
for example, including data bases and knowledge bases:
[ logic_44_n-aryrelations.html ]
Functions and Mappings
[ logic_5_Maps.html ]
Numbers, Lists, and Strings etc
[ logic_6_Numbers..Strings.html ]
Special Logical Systems
For modelling meanings:
[ logic_7_Semantics.html ]
, ontologies and class hierarchies:
[ logic_8_Natural_Language.html ]
, timing, possibilities, and programs:
[ logic_9_Modalities.html ]
The MATHS Theory of Types
[ types.html ]
. . . . . . . . . ( end of section Mathematical Theories) <<Contents | End>>
. . . . . . . . . ( end of section Links to Detailed Theory) <<Contents | End>>
. . . . . . . . . ( end of section Basic Logic For Software Developers) <<Contents | End>>
Notes on MATHS Notation
Special characters are defined in
[ intro_characters.html ]
that also outlines the syntax of expressions and a document.
Proofs follow a natural deduction style that start with assumptions ("Let") and continue to a consequence ("Close Let") and then discard the assumptions and deduce a conclusion. Look here [ Block Structure in logic_2_Proofs ] for more on the structure and rules.
The notation also allows you to create a new network of variables
and constraints, and give them a name. The schema, formal system,
or an elementary piece of documentation starts with "Net" and finishes "End of Net".
For more, see
[ notn_13_Docn_Syntax.html ]
for these ways of defining and reusing pieces of logic and algebra
in your documents.
Notes on the Underlying Logic of MATHS
The notation used here is a formal language with syntax
and a semantics described using traditional formal logic
[ logic_0_Intro.html ]
plus sets, functions, relations, and other mathematical extensions.
For a complete listing of pages by topic see
[ home.html ]