<< Chapter < Page Chapter >> Page >

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.

Economists measure things not in cost, but opportunity cost , the price of something minus the benefits of what you'd get usingthe price for something else. E.g. , for $117 million the university can build a new research center.But what else could you do on campus with $117m?
Historically, logic and rhetoric , the art of persuasion through language, are closely linked.

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
, as well as
…by a path of length 3
,
length 4
, etc.
Write a couple of these sentences!
But trying to write
vertices a and b are connected [by a path of any length]
isn't obvious … in fact, it can be proven that no first-order sentence can express this property! Nor can it express the closely-related property
the graph is connected
(without reference to two named vertices a and b ).

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 , …
. In second-order logic, you can additionally quantify over sets of elements of the domain:
there is a set of numbers, such that …
.

For instance,

for all vertices x and y , there exists a set of vertices (call the set
Red
), the red vertices include a path from x to y
. More precisely,
every Red vertex has exactly two Red neighbors, or it is x or y (which each have exactly 1 red neighbor)
. Is this sentence true exactly when the graph is connected?Why does this description of
red vertices
not quite correspond to
just the vertices on a path from x to y
?

Got questions? Get instant answers now!

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
. (This can be proven, though we won't do so here.)

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
in Java, C++, and C# are based uponuniversal quantification, while
wildcards
in Java are based upon existential quantification.One formalization of this strong link between logic and types is called the Curry-Howard isomorphism .

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
means requires providing the appropriate logical formulas.With hardware, automated verification is now part of the regular practice. However, it is so computationally expensive that it can only be doneon pieces of a design, but not, say, a whole microprocessor. With software, we also frequently work with smaller pieces of code,proving individual functions or algorithms correct. However, there are two big inter-related problems. Many of theproperties we'd like to prove about our software are
undecidable
it is impossible to check the property accurately for every input. Also, specifying full correctness typically requires extensionsto first-order logic, most of which are incomplete. Even something as simple as first-order logic using the integers as our domain andaddition and multiplication as relations is undecidable. Kurt Gödel, 1931 As we've seen, that means that we cannot prove everything we want. While proving hardware and software correct has its limitations, logicprovides us with tools that are still quite useful. For an introduction to one approach used in verification, see TeachLogic's Model-Checking module .

Get Jobilize Job Search Mobile App in your pocket Now!

Get it on Google Play Download on the App Store Now




Source:  OpenStax, Intro to logic. OpenStax CNX. Jan 29, 2008 Download for free at http://cnx.org/content/col10154/1.20
Google Play and the Google Play logo are trademarks of Google Inc.

Notification Switch

Would you like to follow the 'Intro to logic' conversation and receive update notifications?

Ask