Logic: looking back  (Page 2/2)

A much more blatant form of missing information is when the speaker simply chooses to omit it. When arguing for a cause it is standardpractice to simply describe its advantages, without any of its disadvantages or alternatives.

Other logics

You've now been introduced to two logics: propositional and first-order. But, the story does not have to end here.There are many other logics, each with their uses.

Limitations of first-order logic's expressiveness

We can make first-order sentences to express concepts as

vertices $a$ and $b$ are connected by a path of length 2

…by a path of length 3

$\mathrm{length}\le 4$

vertices $a$ and $b$ are connected [by a path of any length]

the graph is connected

Hmm, what about second -order logic? It has a bigger name;whatever it means, perhaps it can express more properties?

What exactly is second-order logic ? In first-order logic, quantifiers range over elements of the domain:

there exist numbers $x$ and $y$ , …

there is a set of numbers, such that …

An interesting phenomenon: There are some relations between how difficult itis to write down a property, and how difficult to compute it! How might you try to formalize the statement

there is a winning strategy for chess

A shortcoming of first-order logic is that it is impossible to express the concept

path

Thus, some other logics used to formalize certain systems include:

• As mentioned, second-order logic is like first-order logic, but it also allowsquantification over entire relations . Thus, you can make formulas that state things like

  For all relations $R$ , if $R$ is symmetric and transitive, then …

  . While less common, we could continue with third-order, fourth-order, etc.
• Temporal logic is based on quantification over time. This is useful to describe how a program's state changes over time.In particular, it is used for describing concurrent program specifications and communication protocols,sequences of communications steps used in security or networking. See, for example, TeachLogic's Model-Checking module .
• Linear logic is a

  resource-aware

  logic. Every premise must be used, but it may be used only once.This models, for example, how keyboard input is usually handled: reading an input also removes it from the input stream, so thatit can't be read again.

Logic in computer science

Logics provide us with a formal language useful for

• specifying properties unambiguously,
• proving that programs and systems do (or don't) have the claimed properties, and
• gaining greater insight into other languages such as database queries .

Programming language type systems are a great example of these first two points. The connectives allow us to talk about pairs and structures ( $x$ and $y$ ), unions ( $x$ or $y$ ), and functions ( if you give the program a $x$ , it produces a $y$ ). The

generics

wildcards

Compilers have very specific logics built into them. In order to optimize your code, analyses check what properties your code has e.g. , are variables $b$ and $c$ needed at the same time, or can they be stored in the same hardware register?

More generally, it would be great to be able to verify that our hardware and software designs were correct.First, specifying what

correct

undecidable