Introduction

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.
• The language for expressing statements has to be very carefully defined, otherwise the task becomes impossible. The result has to be unambiguous, consistent, and a form of readable short hand.
• The reasoning steps will also work on false statements, but there is no guarantee whether the result is true or false. The old Garbage in, Garbage out rule applies.
• So just because you can assume something to be true and derive a consequence that is known to be true, you haven't proven the assumption. You can derive both true and false from false, so true results can come from garbage input.
• Logic shows you how to reason from assumptions to consequences is a very reliable way. It does not tell you how to create the assumptions. Indeed the more precisely we state our assumptions, the more accurately we reason and the more consequences follow. But at the same time that added assumptions reduces the likelihood that the result actually fits with reality.
• If you find a logical system with a precise and restricted set of statements, and these actually seem to fit with reality... perhaps you should (illogically!) be happy with the assumptions.

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

The following describes a particular "generic" logic equivalent to the traditional "Predicate Calculus with Equality". This formalism is used in a range of situations. I assume that it can apply to any type of object. The word type refers to something like a data type in a programming language or an entity type in a data base. The idea is more general however. A type has values, variable, operations, functions, properties, relations, and rules (last but not least) that define what can be assume about it.

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.

Logic

Lower Predicate Calculus with equality

[ logic_10_PC_LPC.html ] [ logic_11_Equality_etc.html ]

Proofs

[ logic_2_Proofs.html ]

Sets

Practical: [ logic_30_Sets.html ] [ logic_31_Families_of_Sets.html ] and Theoretical: [ logic_32_Set_Theory.html ]

Relationships

Binary: relating two objects of different types: [ logic_40_Relations.html ] , of the same type: [ logic_41_HomogenRelations.html ] [ logic_42_Properties_of_Relation.html ]

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 ]

The Notation of MATHS documentation

[ notn_10_Lexicon.html ] [ notn_11_Names.html ] [ notn_12_Expressions.html ] [ notn_13_Docn_Syntax.html ] [ notn_14_Docn_Semantics.html ] [ notn_15_Naming_Documentn.html ] [ notn_2_Structure.html ] [ notn_3_Conveniences.html ] [ notn_4_Re_Use_.html ] [ notn_5_Form.html ] [ notn_6_Algebra.html ] [ notn_7_OO_vs_Algebra.html ] [ notn_8_Evidence.html ] [ notn_dlex.d.html ]

Mathematical Theories

[ home.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

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

For a complete listing of pages by topic see [ home.html ]