text:
The famous Gödel completeness theorem in logic (not to be confused with the even more famous Gödel incompleteness theorem) roughly states the following:

Theorem 1 (Gödel completeness theorem, informal statement) Let ${\Gamma}$ be a first-order theory (a formal language ${{\mathcal L}}$, together with a set of axioms, i.e. sentences assumed to be true), and let ${\phi}$ be a sentence in the formal language. Assume also that the language ${{\mathcal L}}$ has at most countably many symbols. Then the following are equivalent:

• (i) (Syntactic consequence) ${\phi}$ can be deduced from the axioms in ${\Gamma}$ by a finite number of applications of the laws of deduction in first order logic. (This property is abbreviated as ${\Gamma \vdash \phi}$.)
• (ii) (Semantic consequence) Every structure ${{\mathfrak U}}$ which satisfies or models ${\Gamma}$, also satisfies ${\phi}$. (This property is abbreviated as ${\Gamma \models \phi}$.)
• (iii) (Semantic consequence for at most countable models) Every structure ${{\mathfrak U}}$ which is at most countable, and which models ${\Gamma}$, also satisfies ${\phi}$.

One can also formulate versions of the completeness theorem for languages with uncountably many symbols, but I will not do so here. One can also force other cardinalities on the model ${{\mathfrak U}}$ by using the Löwenheim-Skolem theorem.

To state this theorem even more informally, any (first-order) result which is true in all models of a theory, must be logically deducible from that theory, and vice versa. (For instance, any result which is true for all groups, must be deducible from the group axioms; any result which is true for all systems obeying Peano arithmetic, must be deducible from the Peano axioms; and so forth.) In fact, it suffices to check countable and finite models only; for instance, any first-order statement which is true for all finite or countable groups, is in fact true for all groups! Informally, a first-order language with only countably many symbols cannot “detect” whether a given structure is countably or uncountably infinite. Thus for instance even the ZFC axioms of set theory must have some at most countable model, even though one can use ZFC to prove the existence of uncountable sets; this is known as Skolem’s paradox. (To resolve the paradox, one needs to carefully distinguish between an object in a set theory being “externally” countable in the structure that models that theory, and being “internally” countable within that theory.)

Of course, a theory ${\Gamma}$ may contain undecidable statements ${\phi}$ – sentences which are neither provable nor disprovable in the theory. By the completeness theorem, this is equivalent to saying that ${\phi}$ is satisfied by some models of ${\Gamma}$ but not by other models. Thus the completeness theorem is compatible with the incompleteness theorem: recursively enumerable theories such as Peano arithmetic are modeled by the natural numbers ${{\mathbb N}}$, but are also modeled by other structures also, and there are sentences satisfied by ${{\mathbb N}}$ which are not satisfied by other models of Peano arithmetic, and are thus undecidable within that arithmetic.

An important corollary of the completeness theorem is the compactness theorem:

Corollary 2 (Compactness theorem, informal statement) Let ${\Gamma}$ be a first-order theory whose language has at most countably many symbols. Then the following are equivalent:

• (i) ${\Gamma}$ is consistent, i.e. it is not possible to logically deduce a contradiction from the axioms in ${\Gamma}$.
• (ii) ${\Gamma}$ is satisfiable, i.e. there exists a structure ${{\mathfrak U}}$ that models ${\Gamma}$.
• (iii) There exists a structure ${{\mathfrak U}}$ which is at most countable, that models ${\Gamma}$.
• (iv) Every finite subset ${\Gamma'}$ of ${\Gamma}$ is consistent.
• (v) Every finite subset ${\Gamma'}$ of ${\Gamma}$ is satisfiable.
• (vi) Every finite subset ${\Gamma'}$ of ${\Gamma}$ is satisfiable with an at most countable model.

Indeed, the equivalence of (i)-(iii), or (iv)-(vi), follows directly from the completeness theorem, while the equivalence of (i) and (iv) follows from the fact that any logical deduction has finite length and so can involve at most finitely many of the axioms in ${\Gamma}$. (Again, the theorem can be generalised to uncountable languages, but the models become uncountable also.)

There is a consequence of the compactness theorem which more closely resembles the sequential concept of compactness. Given a sequence ${{\mathfrak U}_1, {\mathfrak U}_2, \ldots}$ of structures for ${{\mathcal L}}$, and another structure ${{\mathfrak U}}$ for ${{\mathcal L}}$, let us say that ${{\mathfrak U}_n}$ converges elementarily to ${{\mathfrak U}}$ if every sentence ${\phi}$ which is satisfied by ${{\mathfrak U}}$, is also satisfied by ${{\mathfrak U}_n}$ for sufficiently large ${n}$. (Replacing ${\phi}$ by its negation ${\neg \phi}$, we also see that every sentence that is not satisfied by ${{\mathfrak U}}$, is not satisfied by ${{\mathfrak U}_n}$ for sufficiently large ${n}$.) Note that the limit ${{\mathfrak U}}$ is only unique up to elementary equivalence. Clearly, if each of the ${{\mathfrak U}_n}$ models some theory ${\Gamma}$, then the limit ${{\mathfrak U}}$ will also; thus for instance the elementary limit of a sequence of groups is still a group, the elementary limit of a sequence of rings is still a ring, etc.

Corollary 3 (Sequential compactness theorem) Let ${{\mathcal L}}$ be a language with at most countably many symbols, and let ${{\mathfrak U}_1, {\mathfrak U}_2, \ldots}$ be a sequence of structures for ${{\mathcal L}}$. Then there exists a subsequence ${{\mathfrak U}_{n_j}}$ which converges elementarily to a limit ${{\mathfrak U}}$ which is at most countable.

Proof: For each structure ${{\mathfrak U}_n}$, let ${\hbox{Th}({\mathfrak U}_n)}$ be the theory of that structure, i.e. the set of all sentences that are satisfied by that structure. One can view that theory as a point in ${\{0,1\}^{{\mathcal S}}}$, where ${{\mathcal S}}$ is the set of all sentences in the language ${{\mathcal L}}$. Since ${{\mathcal L}}$ has at most countably many symbols, ${{\mathcal S}}$ is at most countable, and so (by the sequential Tychonoff theorem) ${\{0,1\}^{{\mathcal S}}}$ is sequentially compact in the product topology. (This can also be seen directly by the usual Arzelá-Ascoli diagonalisation argument.) Thus we can find a subsequence ${\hbox{Th}({\mathfrak U}_{n_j})}$ which converges in the product topology to a limit theory ${\Gamma \in \{0,1\}^{{\mathcal S}}}$, thus every sentence in ${\Gamma}$ is satisfied by ${{\mathfrak U}_{n_j}}$ for sufficiently large ${j}$ (and every sentence not in ${\Gamma}$ is not satisfied by ${{\mathfrak U}_{n_j}}$ for sufficiently large ${j}$). In particular, any finite subset of ${\Gamma}$ is satisfiable, hence consistent; by the compactness theorem, ${\Gamma}$ itself is therefore consistent, and has an at most countable model ${{\mathfrak U}}$. Also, each of the theories ${\hbox{Th}({\mathfrak U}_{n_j})}$ is clearly complete (given any sentence ${\phi}$, either ${\phi}$ or ${\neg \phi}$ is in the theory), and so ${\Gamma}$ is complete as well. One concludes that ${\Gamma}$ is the theory of ${{\mathfrak U}}$, and hence ${{\mathfrak U}}$ is the elementary limit of the ${{\mathfrak U}_{n_j}}$ as claimed. $\Box$

[It is also possible to state the compactness theorem using the topological notion of compactness, as follows: let ${X}$ be the space of all structures of a given language ${{\mathcal L}}$, quotiented by elementary equivalence. One can define a topology on ${X}$ by taking the sets ${\{ {\mathfrak U} \in X: {\mathfrak U} \models \phi \}}$ as a sub-base, where ${\phi}$ ranges over all sentences. Then the compactness theorem is equivalent to the assertion that ${X}$ is topologically compact.]

One can use the sequential compactness theorem to build a number of interesting “non-standard” models to various theories. For instance, consider the language ${{\mathcal L}}$ used by Peano arithmetic (which contains the operations ${+, \times}$ and the successor operation ${S}$, the relation ${=}$, and the constant ${0}$), and adjoint a new constant ${N}$ to create an expanded language ${{\mathcal L} \cup \{N\}}$. For each natural number ${n \in {\Bbb N}}$, let ${{\Bbb N}_n}$ be a structure for ${{\mathcal L} \cup \{N\}}$ which consists of the natural numbers ${{\Bbb N}}$ (with the usual interpretations of ${+}$, ${\times}$, etc.) and interprets the symbol ${N}$ as the natural number ${n}$. By the compactness theorem, some subsequence of ${{\Bbb N}_n}$ must converge elementarily to a new structure ${*{\Bbb N}}$ of ${{\mathcal L} \cup \{N\}}$, which still models Peano arithmetic, but now has the additional property that ${N>n}$ for every (standard) natural number ${n}$; thus we have managed to create a non-standard model of Peano arithmetic which contains a non-standardly large number (one which is larger than every standard natural number).

The sequential compactness theorem also lets us construct infinitary limits of various sequences of finitary objects; for instance, one can construct infinite pseudo-finite fields as the elementary limits of sequences of finite fields. I recently discovered that other several correspondence principles between finitary and infinitary objects, such as the Furstenberg correspondence principle between sets of integers and dynamical systems, or the more recent correspondence principles concerning graph limits, can be viewed as special cases of the sequential compactness theorem; it also seems possible to encode much of the sum-product theory in finite fields in an infinitary setting using this theorem. I hope to discuss these points in more detail in a later post. In this post, I wish to review (partly for my own benefit) the proof of the completeness (and hence compactness) theorem. The material here is quite standard (I basically follow the usual proof of Henkin, and taking advantage of Skolemisation), but perhaps the concept of an elementary limit is not as well-known outside of logic as it might be. (The closely related concept of an ultraproduct is better known, and can be used to prove most of the compactness theorem already, thanks to Los’s theorem, but I do not know how to use ultraproducts to ensure that the limiting model is countable. However, one can think (intuitively, at least), of the limit model ${{\mathfrak U}}$ in the above theorem as being the set of “constructible” elements of an ultraproduct of the ${{\mathfrak U}_n}$.)

In order to emphasise the main ideas in the proof, I will gloss over some of the more technical details in the proofs, relying instead on informal arguments and examples at various points.

— 1. Completeness and compactness in propositional logic —

The completeness and compactness theorems are results in first-order logic. But to motivate some of the ideas in proving these theorems, let us first consider the simpler case of propositional logic. The language ${{\mathcal L}}$ of a propositional logic consists of the following:

• A finite or infinite collection ${A_1, A_2, A_3, \ldots}$ of propositional variablesatomic formulae which could be true or false, depending on the interpretation;
• A collection of logical connectives, such as conjunction ${\wedge}$, disjunction ${\vee}$, negation ${\neg}$, or implication ${\implies}$. (The exact choice of which logical connectives to include in the language is to some extent a matter of taste.)
• Parentheses (in order to indicate the order of operations).

Of course, we assume that the symbols used for atomic formulae are distinct from those used for logical connectives, or for parentheses; we will implicitly make similar assumptions of this type in later sections without further comment.

Using this language, one can form sentences (or formulae) by some standard formal rules which I will not write down here. Typical examples of sentences in propositional logic are ${A_1 \implies (A_2 \vee A_3)}$, ${(A_1 \wedge \neg A_1) \implies A_2}$, and ${(A_1 \wedge A_2) \vee (A_1 \wedge A_3)}$. Each sentence is of finite length, and thus involves at most finitely many of the propositional variables. Observe that if ${{\mathcal L}}$ is at most countable, then there are at most countably many sentences.

The analogue of a structure in propositional logic is a truth assignment. A truth assignment ${{\mathfrak U}}$ for a propositional language ${{\mathcal L}}$ consists of a truth value ${A_n^{\mathfrak U} \in \{ \hbox{true}, \hbox{false} \}}$ assigned to each propositional variable ${A_n}$. (Thus, for instance, if there are ${N}$ propositional variables in the language, then there are ${2^N}$ possible truth assignments.) Once a truth assignment ${{\mathfrak U}}$ has assigned a truth value ${A_n^{\mathfrak U}}$ to each propositional variable ${A_n}$, it can then assign a truth value ${\phi^{\mathfrak U}}$ to any other sentence ${\phi}$ in the language ${{\mathcal L}}$ by using the usual truth tables for conjunction, negation, etc.; we write ${{\mathfrak U} \models \phi}$ if ${{\mathfrak U}}$ assigns a true value to ${\phi}$ (and say that ${\phi}$ is satisfied by ${{\mathfrak U}}$), and ${{\mathfrak U} \not \models \phi}$ otherwise. Thus, for instance, if ${A_1^{\mathfrak U} = \hbox{false}}$ and ${A_2^{\mathfrak U} = \hbox{true}}$, then ${{\mathfrak U} \models A_1 \vee A_2}$ and ${{\mathfrak U} \models A_1 \implies A_2}$, but ${{\mathfrak U} \not \models A_2 \implies A_1}$. Some sentences, e.g. ${A_1 \vee \neg A_1}$, are true in every truth assignment; these are the (semantic) tautologies. At the other extreme, the negation of a tautology will of course be false in every truth assignment.

A theory ${\Gamma}$ is a language ${{\mathcal L}}$, together with a (finite or infinite) collection of sentences (also called ${\Gamma}$) in that language. A truth assignment ${{\mathfrak U}}$ satisfies (or models) the theory ${\Gamma}$, and we write ${{\mathfrak U} \models \Gamma}$, if we have ${{\mathfrak U} \models \phi}$ for all ${\phi \in \Gamma}$. Thus, for instance, if ${{\mathfrak U}}$ is as in the preceding example and ${\Gamma := \{ A_1, A_1 \implies A_2 \}}$, then ${{\mathfrak U} \models \Gamma}$.

The analogue of the Gödel completeness theorem is then

Theorem 4 (Completeness theorem for propositional logic) Let ${\Gamma}$ be a theory for a propositional language ${{\mathcal L}}$, and let ${\phi}$ be a sentence in ${{\mathcal L}}$. Then the following are equivalent:

• (i) (Syntactic consequence) ${\phi}$ can be deduced from the axioms in ${\Gamma}$ by a finite number of applications of the laws of propositional logic.
• (ii) (Semantic consequence) Every truth assignment ${{\mathfrak U}}$ which satisfies (or models) ${\Gamma}$, also satisfies ${\phi}$.

One can list a complete set of laws of propositional logic used in (i), but we will not do so here.

To prove the completeness theorem, it suffices to show the following equivalent version.

Theorem 5 (Completeness theorem for propositional logic, again) Let ${\Gamma}$ be a theory for a propositional language ${{\mathcal L}}$. Then the following are equivalent:

• (i) ${\Gamma}$ is consistent, i.e. it is not possible to logically deduce a contradiction from the axioms in ${\Gamma}$.
• (ii) ${\Gamma}$ is satisfiable, i.e. there exists a truth assignment ${{\mathfrak U}}$ that models ${\Gamma}$.

Indeed, Theorem 4 follows from Theorem 5 by applying Theorem 5 to the theory ${\Gamma \cup \{ \neg \phi \}}$ and taking contrapositives.

It remains to prove Theorem 5. It is easy to deduce (i) from (ii), because the laws of propositional logic are sound: given any truth assignment, it is easy to verify that these laws can only produce true conclusions given true hypotheses. The more interesting implication is to obtain (ii) from (i) – given a consistent theory ${\Gamma}$, one needs to produce a truth assignment that models that theory.

Let’s first consider the case when the propositional language ${{\mathcal L}}$ is finite, so that there are only finitely many propositional variables ${A_1,\ldots,A_N}$. Then we can argue using the following “greedy algorithm”.

• We begin with a consistent theory ${\Gamma}$.
• Observe that at least one of ${\Gamma \cup \{ A_1 \}}$ or ${\Gamma \cup \{ \neg A_1 \}}$ must be consistent. For if both ${\Gamma \cup \{ A_1 \}}$ and ${\Gamma \cup \{ \neg A_1 \}}$ led to a logical contradiction, then by the laws of logic one can show that ${\Gamma}$ must also lead to a logical contradiction.
• If ${\Gamma \cup \{A_1\}}$ is consistent, we set ${A_1^{\mathfrak U} := \hbox{true}}$ and ${\Gamma_1 := \Gamma \cup \{A_1\}}$; otherwise, we set ${A_1^{\mathfrak U} := \hbox{false}}$ and ${\Gamma_1 := \Gamma \cup \{\neg A_1\}}$.
• ${\Gamma_1}$ is consistent, so arguing as before we know that at least one of ${\Gamma_1 \cup \{A_2\}}$ or ${\Gamma_1 \cup \{\neg A_2\}}$ must be consistent. If the former is consistent, we set ${A_2^{\mathfrak U} := \hbox{true}}$ and ${\Gamma_2 := \Gamma_1 \cup \{A_2\}}$; otherwise set ${A_2^{\mathfrak U} := \hbox{false}}$ and ${\Gamma_2 := \Gamma_1 \cup \{\neg A_2\}}$.
• We continue in this fashion, eventually ending up with a consistent theory ${\Gamma_N}$ containing ${\Gamma}$, and a complete truth assignment ${{\mathfrak U}}$ such that ${A_n \in \Gamma_N}$ whenever ${1 \leq n \leq N}$ is such that ${A_n^{\mathfrak U} = \hbox{true}}$, and such that ${\neg A_n \in \Gamma_N}$ whenever ${1 \leq n \leq N}$ is such that ${A_n^{\mathfrak U} = \hbox{false}}$.
• From the laws of logic and an induction argument, one then sees that if ${\phi}$ is any sentence with ${\phi^{\mathfrak U} = \hbox{true}}$, then ${\phi}$ is a logical consequence of ${\Gamma_N}$, and hence (since ${\Gamma_N}$ is consistent) ${\neg \phi}$ is not a consequence of ${\Gamma_N}$. Taking contrapositives, we see that ${\phi^{\mathfrak U} = \hbox{false}}$ whenever ${\neg \phi}$ is a consequence of ${\Gamma_N}$; replacing ${\phi}$ by ${\neg \phi}$ we conclude that ${{\mathfrak U}}$ satisfies every sentence in ${\Gamma_N}$, and the claim follows.

Remark 1 The above argument shows in particular that any finite theory either has a model or a proof of a contradictory statement (such as ${A \wedge \neg A}$). Actually producing a model if it exists, though, is essentially the infamous satisfiability problem, which is known to be NP-complete, and thus (if ${P \neq NP}$) would require super-polynomial time to execute.

The case of an infinite language can be obtained by combining the above argument with Zorn’s lemma (or transfinite induction and the axiom of choice, if the set of propositional variables happens to be well-ordered). Alternatively, one can proceed by establishing

Theorem 6 (Compactness theorem for propositional logic) Let ${\Gamma}$ be a theory for a propositional language ${{\mathcal L}}$. Then the following are equivalent:

• (i) ${\Gamma}$ is satisfiable.
• (ii) Every finite subset ${\Gamma'}$ of ${\Gamma}$ is satisfiable.

It is easy to see that Theorem 6 will allow us to use the finite case of Theorem 5 to deduce the infinite case, so it remains to prove Theorem 6. The implication of (ii) from (i) is trivial; the interesting implication is the converse.

Observe that there is a one-to-one correspondence between truth assignments ${{\mathfrak U}}$ and elements of the product space ${\{0,1\}^{\mathcal A}}$, where ${{\mathcal A}}$ is the set of propositional variables. For every sentence ${\phi}$, let ${F_\phi \subset \{0,1\}^{\mathcal A}}$ be the collection of all truth assignments that satisfy ${\phi}$; observe that this is a closed (and open) subset of ${\{0,1\}^{\mathcal A}}$ in the product topology (basically because ${\phi}$ only involves finitely many of the propositional variables). If every finite subset ${\Gamma'}$ of ${\Gamma}$ is satisfiable, then ${\bigcap_{\phi \in \Gamma'} F_\phi}$ is non-empty; thus the family ${(F_\phi)_{\phi \in \Gamma}}$ of closed sets enjoys the finite intersection property. On the other hand, from Tychonoff’s theorem, ${\{0,1\}^{\mathcal A}}$ is compact. We conclude that ${\bigcap_{\phi \in \Gamma} F_\phi}$ is non-empty, and the claim follows.

Remark 2 While Tychonoff’s theorem in full generality is equivalent to the axiom of choice, it is possible to prove the compactness theorem using a weaker version of this axiom, namely the ultrafilter lemma. In fact, the compactness theorem is logically equivalent to this lemma.

— 2. Zeroth-order logic —

Propositional logic is far too limited a language to do much mathematics. Let’s make the language a bit more expressive, by adding constants, operations, relations, and (optionally) the equals sign; however, we refrain at this stage from adding variables or quantifiers, making this a zeroth-order logic rather than a first-order one.

A zeroth-order language ${{\mathcal L}}$ consists of the following objects:

• A (finite or infinite) collection ${A_1, A_2, A_3, \ldots}$ of propositional variables;
• A collection ${R_1, R_2, R_3, \ldots}$ of relations (or predicates), with each ${R_i}$ having an arity (or valence) ${a[R_i]}$ (e.g. unary relation, binary relation, etc.);
• A collection ${c_1, c_2, c_3, \ldots}$ of constants;
• A collection ${f_1, f_2, f_3, \ldots}$ of operators (or functions), with each operator ${f_i}$ having an arity ${a[f_i]}$ (e.g. unary operator, binary operator, etc.);
• Logical connectives;
• Parentheses;
• Optionally, the equals sign ${=}$.

For instance, a zeroth-order language for arithmetic on the natural numbers might include the constants ${0, 1, 2, \ldots}$, the binary relations ${<, \leq , >, \geq}$, the binary operations ${+, \times}$, the unary successor operation ${S}$, and the equals sign ${=}$. A zeroth-order language for studying all groups generated by six elements might include six generators ${a_1,\ldots,a_6}$ and the identity element ${e}$ as constants, as well as the binary operation ${\cdot}$ of group multiplication and the unary operation ${()^{-1}}$ of group inversion, together with the equals sign ${=}$. And so forth.

Note that one could shorten the description of such languages by viewing propositional variables as relations of arity zero, and similarly viewing constants as operators of arity zero, but I find it conceptually clearer to leave these two operations separate, at least initially. As we shall see shortly, one can also essentially eliminate the privileged role of the equals sign ${=}$ by treating it as just another binary relation, which happens to have some standard axioms attached to it.

By combining constants and operators together in the usual fashion one can create terms; for instance, in the zeroth-order language for arithmetic, ${3+(4 \times 5)}$ is a term. By inserting terms into a predicate or relation (or the equals sign ${=}$), or using a propositional variable, one obtains an atomic formula; thus for instance ${3+(4 \times 5) > 25}$ is an atomic formula. By combining atomic formulae using logical connectives, one obtains a sentence (or formula); thus for instance ${((4 \times 5) > 22) \implies (3 + (4\times 5) > 25)}$ is a sentence.

In order to assign meaning to sentences, we need the notion of a structure ${{\mathfrak U}}$ for a zeroth-order language ${{\mathcal L}}$. A structure consists of the following objects:

• A domain of discourse (or universe of discourse) ${\hbox{Dom}({\mathfrak U})}$;
• An assignment of a value ${c_n^{\mathfrak U} \in \hbox{Dom}({\mathfrak U})}$ to every constant ${c_n}$;
• An assignment of a function ${f_n^{\mathfrak U}: \hbox{Dom}({\mathfrak U})^{a[f_n]} \rightarrow \hbox{Dom}({\mathfrak U})}$ to every operation ${f_n}$;
• An assignment of a truth value ${A_n^{\mathfrak U} \in \{ \hbox{true}, \hbox{false}\}}$ to every propositional variable ${A_n}$;
• An assignment of a function ${R_n^{\mathfrak U}: \hbox{Dom}({\mathfrak U})^{a[R_n]} \{ \hbox{true}, \hbox{false}\}}$ to every relation ${R_n}$.

For instance, if ${{\mathcal L}}$ is the language of groups with six generators discussed above, then a structure ${\mathfrak U}$ would consist of a set ${G = \hbox{Dom}({\mathfrak U})}$, seven elements ${a_1^{\mathfrak U},\ldots,a_6^{\mathfrak U}, e^{\mathfrak U} \in G}$ in that set, a binary operation ${\cdot^{\mathfrak U}: G \times G \rightarrow G}$, and a unary operation ${(()^{-1})^{\mathfrak U}: G \rightarrow G}$. At present, no group-type properties are assumed on these operations; the structure here is little more than a magma at this point.

Every sentence ${\phi}$ in a zeroth-order language ${{\mathcal L}}$ can be interpreted in a structure ${{\mathfrak U}}$ for that language to give a truth value ${\phi^{\mathfrak U} \in \{ \hbox{true}, \hbox{false}\}}$, simply by substituting all symbols ${\alpha}$ in the language with their interpreted counterparts ${\alpha^{\mathfrak U}}$ (note that the equals sign ${=}$ does not need any additional data in order to be interpreted). For instance, the sentence ${a_1 \cdot a_2 = a_3}$ is true in ${{\mathfrak U}}$ if ${a_1^{\mathfrak U} \cdot^{\mathfrak U} a_2^{\mathfrak U} = a_3^{\mathfrak U}}$. Similarly, every term ${t}$ in the language can be interpreted to give a value ${t^{\mathfrak U}}$ in the domain of discourse ${\hbox{Dom}({\mathfrak U})}$.

As before, a theory is a collection of sentences; we can define satisfiability ${{\mathfrak U} \models \phi}$, ${{\mathfrak U} \models \Gamma}$ of a sentence ${\phi}$ or a theory ${\Gamma}$ by a structure ${{\mathfrak U}}$ just as in the previous section. For instance, to describe groups with at most six generators in the language ${{\mathcal L}}$, one might use the theory ${\Gamma}$ which consists of all the group axioms, specialised to terms, e.g. ${\Gamma}$ would contain the associativity axioms ${t_1 \cdot (t_2 \cdot t_3) = (t_1 \cdot t_2) \cdot t_3}$ for all choices of terms ${t_1, t_2, t_3}$. (Note that this theory is not quite strong enough to capture the concept of a structure ${{\mathfrak U}}$ being a group generated by six elements, because the domain of ${{\mathfrak U}}$ may contain some “inaccessible” elements which are not the interpretation of any term in ${{\mathcal L}}$, but without the universal quantifier, there is not much we can do in zeroth-order logic to say anything about those elements, and so this is pretty much the best we can do with this limited logic.)

Now we can state the completeness theorem:

Theorem 7 (Completeness theorem for zeroth-order logic) Let ${\Gamma}$ be a theory for a zeroth-order language ${{\mathcal L}}$, and let ${\phi}$ be a sentence in ${{\mathcal L}}$. Then the following are equivalent:

• (i) (Syntactic consequence) ${\phi}$ can be deduced from the axioms in ${\Gamma}$ by a finite number of applications of the laws of zeroth-order logic (i.e. all the laws of first-order logic that do not involve variables or quantifiers).
• (ii) (Semantic consequence) Every truth assignment ${{\mathfrak U}}$ which satisfies (or models) ${\Gamma}$, also satisfies ${\phi}$.

To prove this theorem, it suffices as before to show that every consistent theory ${\Gamma}$ in a zeroth-order logic is satisfiable, and conversely. The converse implication is again straightforward (the laws of zeroth-order logic are easily seen to be sound); the main task is to show the forward direction, i.e.

Proposition 8 Let ${\Gamma}$ be a consistent zeroth-order theory. Then ${\Gamma}$ has at least one model.

Proof: It is convenient to begin by eliminating the equality symbol from the language. Suppose we have already proven Proposition 8 has already been shown for languages without the equality symbol. Then we claim that the proposition also holds for languages with the equality symbol. Indeed, given a consistent theory ${\Gamma}$ in a language ${{\mathcal L}}$ with equality, we can form a companion theory ${\Gamma'}$ in the language ${{\mathcal L}'}$ formed by removing the equality symbol from ${{\mathcal L}}$ and replacing it with a new binary relation ${='}$, by taking all the sentences in ${\Gamma}$ and replacing ${=}$ by ${='}$, and then adding in all the axioms of equality (with ${=}$ replaced by ${='}$) to ${\Gamma'}$. Thus, for instance, one would add the transitivity axioms ${(x =' y) \wedge (y =' z) \implies (x =' z)}$ to ${\Gamma}$ for each triple of terms ${x,y,z}$, as well as substitution axioms such as ${(x =' y) \implies (B(x,z) =' B(y,z))}$ for any terms ${x,y,z}$ and binary functions ${B}$. It is straightforward to verify that if ${\Gamma}$ is consistent, then ${\Gamma'}$ is also consistent, because any contradiction derived in ${\Gamma'}$ can be translated to a contradiction derived in ${\Gamma}$ simply by replacing ${='}$ with ${=}$ throughout and using the axioms of equality. By hypothesis, we conclude that ${\Gamma'}$ has some model ${{\mathfrak U}'}$. By the axioms of equality, the interpretation ${(=')^{{\mathfrak U}'}}$ of ${='}$ in this model is then an equivalence relation on the domain ${\hbox{Dom}({\mathfrak U}')}$ of ${{\mathfrak U}'}$. One can also remove from the domain of ${{\mathfrak U}'}$ any element which is not of the form ${t^{{\mathfrak U}'}}$ for some term ${t}$, as such “inaccessible” elements will not influence the satisfiability of ${\Gamma'}$. We can then define a structure ${{\mathfrak U}}$ for the original language ${{\mathfrak L}}$ by quotienting the domain of ${{\mathfrak U}'}$ by the equivalence relation ${='}$, and also quotienting all the interpretations of the relations and operations of ${{\mathcal L}}$; the axioms of equality ensure that this quotienting is possible, and that the quotiented structure ${{\mathfrak U}}$ satisfies ${{\mathcal L}}$; we omit the details.

Henceforth we assume that ${{\mathcal L}}$ does not contain the equality sign. We will then choose a “tautological” domain of discourse ${\hbox{Dom}({\mathfrak U})}$, by setting this domain to be nothing more than the collection of all terms in the language ${{\mathcal L}}$. For instance, in the language of groups on six generators, the domain ${\hbox{Dom}({\mathfrak U})}$ is basically the free magma (with “inverse”) on six generators plus an “identity”, consisting of terms such as ${(a_1 \cdot a_2)^{-1} \cdot a_1}$, ${(e \cdot a_3) \cdot ((a_4)^{-1})^{-1}}$, etc. With this choice of domain, there is an obvious “tautological” interpretation of constants (${c^{\mathfrak U} := c}$) and operations (e.g. ${B^{\mathfrak U}(t_1, t_2) := B(t_1,t_2)^{\mathfrak U}}$ for binary operations ${B}$ and terms ${t_1,t_2}$), which leads to every term ${t}$ being interpreted as itself: ${t^{\mathfrak U} = t}$.

It remains to figure out how to interpret the propositional variables ${A_1, A_2, \ldots}$ and relations ${R_1, R_2, \ldots}$. Actually, one can replace each relation with an equivalent collection of new propositional variables by substituting in all possible terms in the relation. For instance, if one has a binary relation ${R(,)}$, one can replace this single relation symbol in the language by a (possibly infinite) collection of propositional variables ${R(t_1,t_2)}$, one for each pair of terms ${t_1,t_2}$, leading to a new (and probably much larger) language ${\tilde L}$ without any relation symbols. It is not hard to see that if theory ${\Gamma}$ is consistent in ${{\mathcal L}}$, then the theory ${\tilde \Gamma}$ in ${\tilde L}$ formed by interpreting all atomic formulae such as ${R(t_1,t_2)}$ as propositional variables is also consistent. If ${\tilde \Gamma}$ has a model ${\tilde {\mathfrak U}}$ with the tautological domain of discourse, it is not hard to see that this can be converted to a model ${{\mathfrak U}}$ of ${\Gamma}$ with the same domain by defining the interpretation ${R^{\mathfrak U}}$ of relations ${R}$ in the obvious manner.

So now we may assume that there are no relation symbols, so that ${\Gamma}$ now consists entirely of propositional sentences involving the propositional variables. But the claim now follows from the completeness theorem in propositional logic. $\Box$

Remark 3 The above proof can be viewed as a combination of the completeness theorem in propositional logic and the familiar procedure in algebra of constructing an algebraic object (e.g. a group) that obeys various relations, by starting with the free version of that object (e.g. a free group) and then quotienting out by the equivalence relation generated by those relations.

Remark 4 Observe that if ${{\mathfrak L}}$ is at most countable, then the structures ${{\mathfrak U}}$ constructed by the above procedure are at most countable (because the set of terms is at most countable, and quotienting by an equivalence relation cannot increase the cardinality). Thus we see (as in Theorem 1 or Corollary 2) that if a zeroth-order theory in an at most countable language is satisfiable, then it is in fact satisfiable with an at most countable model.

From the completeness theorem for zeroth-order logic and the above remark we obtain the compactness theorem for zeroth-order logic, which is formulated exactly as in Corollary 2.

— 3. First-order logic —

We are now ready to study languages which are expressive enough to do some serious mathematics, namely the languages of first-order logic, which are formed from zeroth-order logics by adding variables and quantifiers. (There are higher-order logics as well, but unfortunately the completeness and compactness theorems typically fail for these, and they will not be discussed here.)

A language ${{\mathcal L}}$ for a first-order logic consists of the following:

• A (finite or infinite) collection ${A_1, A_2, A_3, \ldots}$ of propositional variables;
• A collection ${R_1, R_2, R_3, \ldots}$ of relations, with each ${R_i}$ having an arity ${a[R_i]}$;
• A collection ${c_1, c_2, c_3, \ldots}$ of constants;
• A collection ${f_1, f_2, f_3, \ldots}$ of operators, with each ${f_i}$ having an arity ${a[f_i]}$;
• A collection ${x_1, x_2, x_3, \ldots}$ of variables;
• Logical connectives;
• The quantifiers ${\forall, \exists}$;
• Parentheses;
• Optionally, the equals sign ${=}$.

For instance, the language for Peano arithmetic includes a constant ${0}$, a unary operator ${S}$, binary operators ${+, \times}$, the equals sign ${=}$, and a countably infinite number of variables ${x_1, x_2, \ldots}$.

By combining constants, variables and operators together one creates terms; by inserting terms into predicates or relations, or using propositional variables, one obtains atomic formulae. These atomic formulae can contain a number of free variables. Using logical connectives as well as quantifiers to bind any or all of these variables, one obtains well-formed formulae; a formula with no free variables is a sentence. Thus, for instance, ${\forall x_2: x_1+x_2=x_2+x_1}$ is a well-formed formula, and ${\forall x_1 \forall x_2: x_1+x_2=x_2+x_1}$ is a sentence.

A structure ${{\mathfrak U}}$ for a first-order language ${{\mathfrak L}}$ is exactly the same concept as for a zeroth-order language: a domain of discourse, together with an interpretation of all the constants, operators, propositional variables, and relations in the language. Given a structure ${{\mathfrak U}}$, one can interpret terms ${t}$ with no free variables as elements ${t^{\mathfrak U}}$ of ${\hbox{Dom}({\mathfrak U})}$, and interpret sentences ${\phi}$ as truth values ${\phi^{\mathfrak U} \in \{ \hbox{true}, \hbox{false}\}}$, in the standard fashion.

A theory is, once again, a collection of sentences in the first-order language ${{\mathcal L}}$; one can define what it means for a structure to satisfy a sentence or a theory just as before.

Remark 5 In most fields of mathematics, one wishes to discuss several types of objects (e.g. numbers, sets, points, group elements, etc.) at once. For this, one would prefer to use a typed language, in which variables, constants, and functions take values in one type of object, and relations and functions take only certain types of objects as input. However, one can easily model a typed theory using a typeless theory by the trick of adding some additional unary predicates to capture type (e.g. ${N(x)}$ to indicate the assertion “${x}$ is a natural number”, ${S(x)}$ to indicate the assertion “${x}$ is a set”, etc.) and modifying the axioms of the theory being considered accordingly. (For instance, in a language involving both natural numbers and other mathematical objects, one might impose a new closure axiom ${\forall x \forall y: N(x) \wedge N(y) \implies N(x+y)}$, and axioms such as the commutativity axiom ${\forall x \forall y: x+y=y+x}$ would need to be modified to ${\forall x \forall y: N(x) \wedge N(y) \implies x+y=y+x}$.) It is a tedious but routine matter to show that the completeness and compactness theorems for typeless first-order logic imply analogous results for typed first-order logic; we omit the details.

To prove the completeness (and hence compactness) theorem, it suffices as before to show that

Proposition 9 Let ${\Gamma}$ be a consistent first-order theory, with an at most countable language ${{\mathcal L}}$. Then ${\Gamma}$ has at least one model ${{\mathcal U}}$, which is also at most countable.

We shall prove this result using a series of reductions. Firstly, we can mimic the arguments in the zeroth-order case and reduce to the case when ${{\mathcal L}}$ does not contain the equality symbol. (We no longer need to restrict the domain of discourse to those elements which can be interpreted by terms, because the universal quantifier ${\forall}$ is now available for use when stating the axioms of equality.) Henceforth we shall assume that the equality symbol is not present in the language.

Next, by using the laws of first-order logic to push all quantifiers in the sentences in ${\Gamma}$ to the beginning (e.g. replacing ${(\forall x: P(x)) \wedge (\forall y: Q(y))}$ with ${\forall x \forall y: P(x) \wedge Q(y)}$) one may assume that all sentences in ${\Gamma}$ are in prenex normal form, i.e. they consist of a “matrix” of quantifiers, followed by an quantifier-free formula – a well-formed formula with no quantifiers. For instance, ${\forall x \exists y \forall z \exists w: P(x,y,z,w)}$ is in prenex normal form, where ${P(x,y,z,w)}$ is an quantifier-free formula with four free variables ${x,y,z,w}$.

Now we will start removing the existential quantifiers ${\exists}$ from the sentences in ${\Gamma}$. Let’s begin with a simple case, when ${\Gamma}$ contains a sentence of the form ${\exists x: P(x)}$ for some quantifier-free formula of one free variable ${x}$. Then one can eliminate the existential quantifier by introducing a witness, or more precisely adjoining a new constant ${c}$ to the language ${{\mathcal L}}$ and replacing the statement ${\exists x: P(x)}$ with the statement ${P(c)}$, giving rise to a new theory ${\Gamma'}$ in a new language ${\Lambda'}$. The consistency of ${\Gamma}$ easily implies the consistency of ${\Gamma'}$, while any at most countable model for ${\Gamma'}$ can be easily converted to an at most countable model for ${\Gamma}$ (by “forgetting” the symbol ${c}$). (In fact, ${\Gamma'}$ is a conservative extension of ${\Gamma}$.) We can apply this reduction simultaneously to all sentences of the form ${\exists x: P(x)}$ in ${\Gamma}$ (thus potentially expanding the collection of constants in the language by a countable amount).

The same argument works for any sentence in prenex normal form in which all the existential quantifiers are to the left of the universal quantifiers, e.g. ${\exists x \exists y \forall z \forall w: P(x,y,z,w)}$; this statement requires two constants to separately witness ${x}$ and ${y}$, but otherwise one proceeds much as in the previous paragraph. But what about if one or more of the existential quantifiers is buried behind a universal quantifier? The trick is then to use Skolemisation. We illustrate this with the simplest case of this type, namely that of a sentence ${\forall x \exists y: P(x,y)}$. Here, one cannot use a constant witness for ${y}$. But this is no problem: one simply introduces a witness that depends on ${x}$. More precisely, one adjoins a new unary operator ${c}$ to the language ${{\mathcal L}}$ and replaces the statement ${\forall x \exists y: P(x,y)}$ by ${\forall x: P(x,c(x))}$, creating a new theory ${\Gamma'}$ in a new language ${\Lambda'}$. One can again show (though this is not entirely trivial) that the consistency of ${\Gamma}$ implies the consistency of ${\Gamma'}$, and that every countable model for ${\Gamma'}$ can be converted to a countable model for ${\Gamma}$ (again by “forgetting” ${c}$). So one can eliminate the existential quantifier from this sentence also. Similar methods work for any other prenex normal form; for instance with the sentence

$\displaystyle \forall x \exists y \forall z \exists w: P(x,y,z,w)$

one can obtain a conservative extension of that theory by introducing a unary operator ${c}$ and a binary operator ${d}$ and replacing the above sentence with

$\displaystyle \forall x \forall z: P( x, c(x), z, d( x, z) ).$

One can show that one can perform Skolemisation on all the sentences in ${\Gamma}$ simultaneously, which has the effect of eliminating all existential quantifiers from ${\Gamma}$ while still keeping the language ${{\mathcal L}}$ at most countable (since ${\Gamma}$ is at most countable). (Intuitively, what is going on here is that we are interpreting all existential axioms in the theory as implicitly defining functions, which we then explicitly formalise as a new symbol in the language. For instance, if we had some theory of sets which contained the axiom of choice (every family of non-empty sets ${(X_\alpha)_{\alpha \in A}}$ admits a choice function ${f: A \rightarrow \bigcup_{\alpha \in A} X_\alpha}$), then we can Skolemise this by introducing a “choice function function” ${{\mathcal F}: (X_\alpha)_{\alpha \in A} \mapsto {\mathcal F}( (X_\alpha)_{\alpha \in A} )}$ that witnessed this axiom to the language. Note that we do not need uniqueness in the existential claim in order to be able to perform Skolemisation.)

After performing Skolemisation and adding all the witnesses to the language, we are reduced to the case in which all the sentences in ${\Gamma}$ are in fact universal statements, i.e. of the form ${\forall x_1 \ldots \forall x_k: P(x_1,\ldots,x_k)}$, where ${P(x_1,\ldots,x_k)}$ is an quantifier-free formula of ${k}$ free variables. In this case one can repeat the zeroth-order arguments, selecting a structure ${{\mathfrak U}}$ whose domain of discourse is the tautological one, indexed by all the terms with no free variables (in particular, this structure will be countable). One can then replace each first-order statement ${\forall x_1 \ldots \forall x_k: P(x_1,\ldots,x_k)}$ in ${\Gamma}$ by the family of zeroth-order statements ${P(t_1,\ldots,t_k)}$, where ${t_1,\ldots,t_k}$ ranges over all terms with no free variables, thus creating a zeroth-order theory ${\Gamma_0}$. As ${\Gamma}$ is consistent, ${\Gamma_0}$ is also, so by the zeroth-order theory, we can find a model ${{\mathfrak U}}$ for ${\Gamma_0}$ with the tautological domain of discourse, and it is clear that this structure will also be a model for the original theory ${\Gamma}$. The proof of the completeness theorem (and thus the compactness theorem) is now complete.

In summary: to create a countable model from a consistent first-order theory, one first replaces the equality sign ${=}$ (if any) by a binary relation ${='}$, then uses Skolemisation to make all implied functions and operations explicit elements of the language. Next, one makes the zeroth-order terms of the new language the domain of discourse, applies a greedy algorithm to decide the truth assignment of all zeroth-order sentences, and then finally quotients out by the equivalence relation given by ${='}$ to recover the countable model.

Remark 6 I find the use of Skolemisation to greatly clarify, at a conceptual level, the proof of the completeness theorem. However, at a technical level it does make things more complicated: in particular, showing that the Skolemisation of a consistent theory is still consistent does require some non-trivial effort (one has to take all arguments involving the Skolem function ${c()}$, and replace every occurence of ${c()}$ by a “virtual” function, defined implicitly using existential quantifiers). On the other hand, this fact is easy to prove once one already has the completeness theorem, though we of course cannot formally take advantage of this while trying to prove that theorem!

The more traditional Henkin approach is based instead on adding a large number of constant witnesses, one for every existential statement: roughly speaking, for each existential sentence ${\exists x: P(x)}$ in the language, one adds a new constant ${c}$ to the language and inserts an axiom ${(\exists x: P(x)) \implies P(c)}$ to the theory; it is easier to show that this preserves consistency than it is with a more general Skolemisation. Unfortunately, every time one adds a constant to the language, one increases the number of existential sentences for which one needs to perform this type of witnessing, but it turns out that after applying this procedure a countable number of times, one can get to the point where every existential sentence is automatically witnessed by some constant. This has the same ultimate effect as Skolemisation, namely one can convert sentences containing existential quantifiers to ones which are purely universal, and so the rest of the proof is much the same as the proof described above. On the other hand, the Henkin approach avoids the axiom of choice (though one still must use the ultrafilter lemma, of course).


text:
Bolt Group Coefficient for Eccentric Loads - Maple Programming Help

Home : Support : Online Help : Applications and Example Worksheets : Science and Engineering : applications/BoltGroupCoefficient

Bolt Group Coefficient for Eccentric Loads

Introduction

This application calculates the bolt coefficient for eccentrically loaded bolt groups using the Instantaneous Center of Rotation method (also known as the Ultimate Strength method).

The bolt coefficient C is the ratio of the factored force (or available strength) of the bolt group Pu and the shear capacity of a single bolt $\mathrm{φr__n}$,

Once the coefficient is known, a bolt group can be designed for any load.

Traditionally, bolt group coefficients are extracted by using tabulated values in the AISC Steel Construction Manual. However, these tables are limited to common bolt patterns, and specific load eccentricities and angles. Non-tabulated values must be extracted by using linear interpolation.

This Maple worksheet, however, calculates the bolt group coefficient for any bolt and load configuration by implementing the theory used to generate the tables.

The results agree with those presented in AISC Manual of Steel Construction: Load and Resistance Factor Design, 2nd Edition.

 >

Parameters

The following commands define the bolt locations and plot them.

 > $\mathrm{boltLoc}≔⟨⟨-1.5|-3⟩,⟨1.5|-3⟩,⟨-1.5|0⟩,⟨1.5|0⟩,⟨-1.5|3⟩,⟨1.5|3⟩⟩⟦\mathrm{inch}⟧:$
 > $\mathrm{plot}\left(\mathrm{convert}~~\left(\mathrm{boltLoc},\mathrm{unit_free}\right),\mathrm{style}=\mathrm{point},\mathrm{symbol}=\mathrm{solidcircle},\mathrm{symbolsize}=40\right)$

The shear strength of a single bolt (kip):

 > $\mathrm{φr__n}≔96081⟦\mathrm{N}⟧:$

The horizontal component of force eccentricity with respect to the centroid of bolt group (in):

 > $\mathrm{e__h}≔2⟦\mathrm{inch}⟧:$

Force angle to horizontal axis (deg):

 >
 ${\mathrm{\beta }}{≔}{1.308996939}$ (2.1)

Calculations

Translate the bolt locations so that the centroid is at the origin.

 >

The eccentricity:

 >
 ${\mathrm{e}}{≔}{1.931851653}{}⟦{\mathrm{in}}⟧$ (3.1)

 > $\mathrm{\beta }≔\left|\left\{\begin{array}{cc}\mathrm{\beta }& \mathrm{e}>0\\ \mathrm{\beta }+0.5\mathrm{\pi }& \mathrm{otherwise}\end{array}\right\\right|$
 ${\mathrm{\beta }}{≔}{1.308996939}$ (3.2)

Instantaneous center of rotation (ICR):

 >
 >

Bolt angle to ICR (rad):

 >

Bolt distance to ICR (inches):

 >

Bolt displacement (inches) from Crawford and Kulak (1971):

 > $\mathrm{Δ}≔\frac{\mathrm{d}}{~\mathrm{dmax}}\cdot 0.34:$

Load-deformation relationship from Crawford and Kulak (1971):

 > $\mathrm{Rn}≔\mathrm{φr__n}\cdot {\left(1-~{ⅇ}^{~\left(-10\cdot \mathrm{\Delta }\right)}\right)}^{~0.55}:$

Optimization

The sums of the bolt forces in the vertical and horizontal directions are equal to the applied shear and axial loads.

 >

The moment of the bolt forces about the ICR is equal to the moment of the applied load.

 >
 > $\mathrm{res}≔\mathrm{fsolve}\left(\left\{\mathrm{forceX},\mathrm{forceY},\mathrm{moment}\right\},\left\{\mathrm{P__0}=1⟦\mathrm{N}⟧,\mathrm{m__0}=1⟦\mathrm{m}⟧,\mathrm{L__0}=1⟦\mathrm{m}⟧\right\}\right)$
 ${\mathrm{res}}{≔}\left\{\mathrm{L__0}{=}{0.09115169826}{}⟦{\mathrm{m}}⟧{,}\mathrm{P__0}{=}{429160.9378}{}⟦{\mathrm{N}}⟧{,}\mathrm{m__0}{=}{-}{0.004661726525}{}⟦{\mathrm{m}}⟧\right\}$ (4.1)

Results

Ultimate tensile strength of bolt group

 > $\mathrm{P__u}≔\mathrm{eval}\left(\mathrm{P__0},{\mathrm{res}}_{2}\right)$
 $\mathrm{P__u}{≔}{429160.9378}{}⟦{\mathrm{N}}⟧$ (5.1)

Bolt coefficient:

 > $\mathrm{C}≔\frac{\mathrm{P__u}}{\mathrm{φr__n}}$
 ${\mathrm{C}}{≔}{4.466657693}$ (5.2)
 >
 References Behavior of eccentrically loaded bolted connections, Crawford S. F., Kulak, G. L. (1968) AISC Manual of Steel Construction: Load and Resistance Factor Design 2nd Edition
 >

format: plain


text:
# zbMATH — the first resource for mathematics

Equivariant Bauer-Furuta invariants on some connected sums of 4-manifolds. (English) Zbl 1421.57041
Summary: On some connected sums of 4-manifolds with natural actions of finite groups, we use equivariant Bauer-Furuta invariant to deduce the existence of solutions of Seiberg-Witten equations invariant under the group actions.
For example, for any integer $$k\geq 2$$ we show that the connected sum of $$k$$ copies of a 4-manifold $$M$$ with nontrivial Bauer-Furuta invariant has a nontrivial $$\mathbb{Z}_k$$-equivariant Bauer-Furuta invariant for the obviously glued Spin$$^c$$ structure, where the $$\mathbb{Z}_k$$-action cyclically permutes $$k$$ summands of $$M$$. This contrasts with the fact that ordinary Bauer-Furuta invariants of such connected sums are all trivial for any sufficiently large $$k$$, when $$b_1(M)=0$$.
##### MSC:
 57R57 Applications of global analysis to structures on manifolds 57M60 Group actions on manifolds and cell complexes in low dimensions
Full Text:


text:
Sciencemadness Discussion Board » Fundamentals » Miscellaneous » Dangers/risks of Mazilli ZVS driver? Select A Forum Fundamentals   » Chemistry in General   » Organic Chemistry   » Reagents and Apparatus Acquisition   » Beginnings   » Responsible Practices   » Miscellaneous   » The Wiki Special topics   » Technochemistry   » Energetic Materials   » Biochemistry   » Radiochemistry   » Computational Models and Techniques   » Prepublication Non-chemistry   » Forum Matters   » Legal and Societal Issues

Pages:  1  2    4
Author: Subject: Dangers/risks of Mazilli ZVS driver?
woelen

Posts: 7582
Registered: 20-8-2005
Location: Netherlands
Member Is Offline

Mood: interested

I made a completely new ZVS driver with IRFP260s, 5 W 470 Ohm ceramic resistors, 10 kOhm metalfilm resistors, 13 V zener diodes and hand wound choke inductor on yellow/white powdered iron core. I used a flyback transformer (old Nokia thing), with a DC cascade at its output. The result with the new ZVS driver is quite impressive. From a fixed 13.8 V power supply it starts sparking at 2 cm distance! The only strange thing is that I have many fat and very noisy sparks per second from the cascade and not a smooth arc. I think I have 10 or so fat sparks. Probably, the cascade contains a capacitor at its output, which is charged every 100 ms or so.

Anyway, this driver is much better than the previous one. It looks ugly though. The PCB I ordered was not made for the components I used (e.g. the diodes, suggested by IrC have very thick wires, which cannot go through the drilled hole in the PCB, the resistors I have are intended for lying on a PCB, while the PCB is designed for resistors which can stand on the PCB). So, I needed quite a lot of tinkering and improvising before I had a working driver. So, mechanically it is of much less quality, but electrically it is superior.

Btw, I replaced the 470 nF capacitor by a 330 nF one. I don't have 630V 470 nF capacitors anymore, but I have plenty of 330 nF/2 kV and 1 uF/630 V. I chose to take the 330 nF one. I have room left on the PCB to add another one in parallel to the one I already added.

I also noticed that the new circuit uses a remarkably low current. After I switch off my power supply it keeps on sparking for well over a second or so, while the power supply only has a 47000 uF capacitor behind its rectifier. The previous version of the driver immediately stopped generating sparks with the same flyback/cascade device when the power supply was switched off.

[Edited on 15-9-14 by woelen]

The art of wondering makes life worth living...
Want to wonder? Look at https://woelen.homescience.net
seilgu
Harmless

Posts: 13
Registered: 24-10-2014
Member Is Offline

Mood: No Mood

latchup

Has anybody found a way to improve the circuit so it doesn't latchup and blow mosfets?

I've built this circuit years ago and it worked fine, recently I brought it out and found that if the power supply doesn't rise fast enough, the circuit latches up and one mosfet conducts heavily, while the other one remains shut off. I'm using a linear benchtop supply so current it limited to 3A and no mosfet were blown.

I'm not sure I understand this circuit correctly. When powered up, the voltage on both mosfets will rise to about 3V, and one of them (A) will start to conduct more first. At this point the current from the power supply will flow both sides, because the capacitor is being charged on the B side. The positive feedback will turn mosfet A fully on, thus shutting mosfet B fully off.

Suppose the B side now charges fully, and current stops flowing into the B side. If the center tap of the inductor is at voltage V, then since mosfet A is at 0V, mosfet B would be at 2V. The current through A side will continue to increase following V = L*dI/dt, until either the supply limits or the inductor saturates.

If the supply is limited, the inductor current will have to come from the B side, thus starting the cycle. However if it is due to saturated inductor, it just means the L value becomes small, thus the supply will have to provide larger dI/dt. Therefore the need for a RFC choke on the supply.

Still can't see why latchup occurs....

Metacelsus
International Hazard

Posts: 2480
Registered: 26-12-2012
Location: Boston, MA
Member Is Offline

Mood: Double, double, toil and trouble

I've never had latchup problems on the circuit I built, although I have heard of others having them. They seem to be mitigated by proper gate resistor adjustment. What values of resistors are you using on the MOSFET gates, and how big is your inductor?

As below, so above.
seilgu
Harmless

Posts: 13
Registered: 24-10-2014
Member Is Offline

Mood: No Mood

latchup

I used a ferrite-core 47uH (marked as that, didn't test). Today I replaced it with higher inductance and the latchup problem is mitigated. If I use a very large inductor it doesn't latchup (but of course it would reduce the power output).

resistor values are as the original, 470 and 10k.

What might be the reason behind this?

[Edited on 24-10-2014 by seilgu]
WGTR
International Hazard

Posts: 948
Registered: 29-9-2013
Location: Online
Member Is Offline

Mood: Outline

 Quote: Originally posted by seilgu Has anybody found a way to improve the circuit so it doesn't latchup and blow mosfets? I've built this circuit years ago and it worked fine, recently I brought it out and found that if the power supply doesn't rise fast enough, the circuit latches up and one mosfet conducts heavily, while the other one remains shut off. I'm using a linear benchtop supply so current it limited to 3A and no mosfet were blown. I'm not sure I understand this circuit correctly. When powered up, the voltage on both mosfets will rise to about 3V, and one of them (A) will start to conduct more first. At this point the current from the power supply will flow both sides, because the capacitor is being charged on the B side. The positive feedback will turn mosfet A fully on, thus shutting mosfet B fully off. Suppose the B side now charges fully, and current stops flowing into the B side. If the center tap of the inductor is at voltage V, then since mosfet A is at 0V, mosfet B would be at 2V. The current through A side will continue to increase following V = L*dI/dt, until either the supply limits or the inductor saturates. If the supply is limited, the inductor current will have to come from the B side, thus starting the cycle. However if it is due to saturated inductor, it just means the L value becomes small, thus the supply will have to provide larger dI/dt. Therefore the need for a RFC choke on the supply. Still can't see why latchup occurs....

I posted something earlier in the thread here:
Successful startup depends on there being a slight difference between the two MOSFETs, with a fast rise time in the power supply voltage. If this is not possible, then noise injected into the gates may be necessary to get it started (hopefully before the device melts down).

What supply voltage are you using? 3V? If so, you need quite a bit more than that, depending on the gate threshold of your MOSFETs. It's possible that one is turning on, while another isn't, due to part variations.

Personally, I prefer designs that consume no power when there is no gate drive. They are much safer.
seilgu
Harmless

Posts: 13
Registered: 24-10-2014
Member Is Offline

Mood: No Mood

latchup

There is always going to a slight difference between the MOSFETs, I heard somebody saying that for the noise to start the oscillation, the feedback gain should be larger than 1.
I don't understand how it works tho. Assuming gate A has a noise of exp(-iwt), that would translate to the drain current in the same phase, the gain determined by the V_GS to I_DD diagram in the datasheet of the MOSFET. Now assuming w is the LC tank frequency, that would mean the parallel LC tank looks like a infinite resistance to the exp(-iwt) noise, therefore the gain at mosfet B should be infinite! Why doesn't this start the oscillation?

My supply voltage is slow rising because I manually turn up the regulated voltage. It's well above 3V of course, the supply has a max voltage of ~45V.

I'm looking for some improvements for this circuit, of course one way is to use a 555 timer and if one mosfet latchups too long it would reset the circuit. Since I'm only using it for small powers I don't really need that actually...
Metacelsus
International Hazard

Posts: 2480
Registered: 26-12-2012
Location: Boston, MA
Member Is Offline

Mood: Double, double, toil and trouble

You could just put a switch between the supply and the circuit, and turn it on once you've set the voltage.

As below, so above.
seilgu
Harmless

Posts: 13
Registered: 24-10-2014
Member Is Offline

Mood: No Mood

latchup

That is a solution, but not a robust one.

For example if the load is suddenly changed it might still go into latchup mode. Therefore a protection circuit or a guaranteed oscillating design is still preferred. Also it could save lots of mosfets for newbies..
WGTR
International Hazard

Posts: 948
Registered: 29-9-2013
Location: Online
Member Is Offline

Mood: Outline

On slow power supply ramp up, if both MOSFETs conduct at the same time, the tank circuit is effectively shorted out. This means it has practically no inductance, if the windings are well-coupled. (Temporary) current limiting now depends on the series choke, which will probably saturate more quickly than you can ramp the supply voltage. At that point you have a big, saturated, steaming pile of silicon and ferrite (unless you have a current-limited power supply, under which conditions it merely simmers with mild annoyance).

To make this work, the series choke needs to be able to handle without saturating whatever current the power supply can deliver. Also, the gate drive to both MOSFETs needs to be kept at zero when the device is not oscillating. This latter point is the opposite of how a typical Mazilli driver works, as it supplies gate drive to both devices on power up, and relies on one device out-competing the other to get oscillation going. If oscillation doesn't start, well, then both devices smoke.

Think about this: given that both MOSFETs should be "OFF" when not oscillating, but with the functioning circuit remaining within the design constraints of a Mazilli-type design, could you modify the design to work with, say, a temporary pushbutton that could get the oscillator started? And a circuit that, if it stopped oscillating under load, would allow the gate drive to drift to zero?

seilgu
Harmless

Posts: 13
Registered: 24-10-2014
Member Is Offline

Mood: No Mood

 Quote: Originally posted by WGTR On slow power supply ramp up, if both MOSFETs conduct at the same time, the tank circuit is effectively shorted out. This means it has practically no inductance, if the windings are well-coupled. (Temporary) current limiting now depends on the series choke, which will probably saturate more quickly than you can ramp the supply voltage. At that point you have a big, saturated, steaming pile of silicon and ferrite (unless you have a current-limited power supply, under which conditions it merely simmers with mild annoyance). To make this work, the series choke needs to be able to handle without saturating whatever current the power supply can deliver. Also, the gate drive to both MOSFETs needs to be kept at zero when the device is not oscillating. This latter point is the opposite of how a typical Mazilli driver works, as it supplies gate drive to both devices on power up, and relies on one device out-competing the other to get oscillation going. If oscillation doesn't start, well, then both devices smoke. Think about this: given that both MOSFETs should be "OFF" when not oscillating, but with the functioning circuit remaining within the design constraints of a Mazilli-type design, could you modify the design to work with, say, a temporary pushbutton that could get the oscillator started? And a circuit that, if it stopped oscillating under load, would allow the gate drive to drift to zero?

I don't think there is the remote possibility of both MOSFETs smoking. When one turns on it immediately turns the other off, they can't be on at the same time.
They can't be both off, either. When not oscillating, one is on and the other is off, and it doesn't switch.

The way to get is restarted is for the feedbackloop to have a gain larger than 1 at the desired frequency so that any noise of the frequency will get amplified.
The other way to prevent latchup is to detect latchup either by checking how long the MOSFETs turn on or how hot the thing gets. Although if used with large power supplies, you'd be already too late when it feels hot.
WGTR
International Hazard

Posts: 948
Registered: 29-9-2013
Location: Online
Member Is Offline

Mood: Outline

 Quote: Originally posted by seilgu I don't think there is the remote possibility of both MOSFETs smoking. When one turns on it immediately turns the other off, they can't be on at the same time. They can't be both off, either. When not oscillating, one is on and the other is off, and it doesn't switch.

It depends a lot on the ratio of FET "ON" resistance to the tank coil DC resistance. If this ratio is high, then when not oscillating the voltage on both drains will be about equal. If the circuit latches up with one driver off (like you mentioned), then the winding resistance of the tank coil is relatively high (especially since the supply is limited to 3A).

If I understand your previous posts correctly, the power supply goes into current limiting at 3A, supplying 3V when the circuit is latched up. This would imply that there are about 2 ohms DC resistance across the whole winding. Can you measure it?

 Quote: Originally posted by seilgu The way to get is restarted is for the feedbackloop to have a gain larger than 1 at the desired frequency so that any noise of the frequency will get amplified. The other way to prevent latchup is to detect latchup either by checking how long the MOSFETs turn on or how hot the thing gets. Although if used with large power supplies, you'd be already too late when it feels hot.

Yes, loop gain greater than +1 is needed for oscillation at the frequency of interest, but when the drivers latch up, the FETs are no longer operating in a linear range. At that point there is practically no small-signal amplification. Thermal noise won't be enough to get it going.

If you want to try getting this to work, I would suggest as a first step to decrease the tank winding resistance enough that both FETs turn on when the circuit is not oscillating, and the drain voltages are approximately equal. Second, add two small inductors in series with either side of the tank coil, with a small percentage of the overall reactance. Thirdly, make sure that none of the magnetics are saturating with your 3A supply.

I'm getting tired enough right now that I am beginning to hallucinate that chipmunks are telling me what to write. That must mean that I need to go to bed.
violet sin
International Hazard

Posts: 1357
Registered: 2-9-2012
Location: Back yard staring at stars
Member Is Offline

Mood: Good

So I've been working on a zvs driver myself. Finally decided to put together parts that I bought a few years back not sure if they are all in the same category of power consumption for the proper circuit. Parts are as follows: mosfet- IRFP250N, fast diode- UF4007, zen diode- 1N-5349B, 1uF MKP10 cap 1000-600~, 5w 470 ohm, 1/4w 10k ohm,

Ended up copying an online schematic and making my own PCB board. Got everything etched and soldered in place except for the inductor coil. For a non electronics guy some of this stuff is kind of hard to pick up, like figuring out on the parameters to wind your own. I can usually gather enough info just reading online, but lately life gives me my spare time in numerous shorter lengths. While working away I only get to use my cell phone for internet Leads to learning simple things many times over, and little time for theory.

Any suggestions for whether or not the yellow/white T106-26 core would be good? Pretty sure it was from a ATX PSU.
I do have T 106 26 white yellow iron powder core, a few ferrite cores unmarked and bare. I also have three spools of magnet wire from RadioShack the thickest is 22 gauge but I do also have 26 and 30 gauge

Also, etching.g was done pretty easily. One SOS pad, muriatic acid, little bit of rust and some hydrogen peroxide 3%. The solution was ready in about half an hour, and etched rather rapidly. 10 minutes was almost too long as the traces we're getting undercut.

Any input on the inductor core would be great, so far the online calculators I am seeing say between 38 and 42 raps on the core with the 22 gauge wire that I have( for about 150 uH). But the schematic that I had only states between 47 and 200 Micro Henrys of inductance, is a pretty wide open guess for someone who doesn't have the know-how or eyes for mismatch problem.

I have a fly back to try it on, but will eventually be building an induction heater. I don't reall need big sparks for fun, But melting metal sounds productive

IrC
International Hazard

Posts: 2710
Registered: 7-3-2005
Location: Eureka
Member Is Offline

Mood: Discovering

100 uH might be fine but safer to go with 150 uH, or you risk the circuit not starting. This can result in the mosfets turned on steady, blowing them. As to the gauge 22 is OK if you do not plan on more than 5 amps DC input. You need to determine what maximum wattage rating you wish to have and go from there as to the chokes current handling ability. If you plan on metal melting you need to go for a kilowatt design at least so your choke would need a better current rating. For example at 24 volts you need a choke able to handle over 42 amperes while being a minimum of 150 uH. I use 100 uH often because I had a good quantity but I have turned it on and blown mosfets a few times. I do not know why they would have given a range as low as 47 uH, unless they also make a living selling parts. Keep in mind the choke must handle whatever total current you will see and if I had to pick a minimum inductance it would be around 120 uH to guarantee starting every time power is applied. The yellow core shown should be fine for what you are doing right now. You want a core large enough to take enough turns at the wire size you choose to reach the required inductance, and consider in high power designs core saturation. I should also mention you can reduce the current requirement if you operate at higher voltages such as 48 volts instead of 24. However you must consider shrapnel protection from exploding parts, the circuit starts to become really dangerous as you operate on higher voltages. You mention 1 uF, I found better efficiency at 0.33 to 0.66 uF for the circuits I built operating under 1KW. Be sure to over rate the voltage, this component likes to explode. I have had them sound like a shotgun blast leaving dents in shielding. Very dangerous especially in the 50 volt and higher power input range.

"Science is the belief in the ignorance of the experts" Richard Feynman
violet sin
International Hazard

Posts: 1357
Registered: 2-9-2012
Location: Back yard staring at stars
Member Is Offline

Mood: Good

Thanks for the help there IrC, much appreciated. I cut wire to the specs of the coil calculator and came up a couple turns shy of the 150uH rating. ~135 as it was two turns under 150 and two turns over 120. By online calculator, my multimeter isn't that multiple in function soon enough.

It's all wound, soldered, the 5+5 on fly back done... Be home tomorrow to throw it on a power supply

Then on to the next planning stage, the induction heater. Side note, solder or flux seems to be eating my irons rather rapidly. Butane one I've had for years and a new harbor freight one see damage immediately. Not a fan of that.
IrC
International Hazard

Posts: 2710
Registered: 7-3-2005
Location: Eureka
Member Is Offline

Mood: Discovering

"Science is the belief in the ignorance of the experts" Richard Feynman
violet sin
International Hazard

Posts: 1357
Registered: 2-9-2012
Location: Back yard staring at stars
Member Is Offline

Mood: Good

I've been totally baffled, everything was soldered, checked.powered up and NOTHING! 're-checked, hair pulled out, hours of pouring over the net... Took some of the spare parts and wired up the bare lead (no PCB) version seen online, NOTHING! Removed one primary winding off each side, nope, wound on heavier solid wire on another fly back, nada. More of the same, reading, checking, polarity, all diodes checked after dissasembly, all fine. So I measured to see I'd the 470 ohm 5W resistors had taken a beating before I put them away,.. set multimeter to 2000ohm setting, ol reading?? So I thought wow, it got destroyed, scaled up meter setting to see what was going on... 470 "K" ohm !?!?! F-u eBay, just F-u... Not the first time I've gotten wrong bits.

Best to keep on top of those guys,.and measure everything you get. Well, now I have one taken apart, and one MOSTLY still on its PCB. Need some correct power resistors... Kinda pissed, but better to know. Check back in when it's sorted

Metacelsus
International Hazard

Posts: 2480
Registered: 26-12-2012
Location: Boston, MA
Member Is Offline

Mood: Double, double, toil and trouble

That's why I use Digikey instead of eBay (which is just too unreliable). At least the bad resistors didn't cause any other components to fail.

As below, so above.
WGTR
International Hazard

Posts: 948
Registered: 29-9-2013
Location: Online
Member Is Offline

Mood: Outline

Unfortunately, I can see from the pictures that you do in fact have 470k resistors. Look at the bright side: you already have a pair of 470k parts for something else! They don't go bad sitting in the junk box.

I looked at a data sheet for the capacitor that you have: http://www.mouser.com/ds/2/440/WIMA_MKP_10-3387.pdf. It's rated for pulse applications, but information about its RMS current handling capability isn't given. I use these types of capacitors for general medium current RF applications: http://www.mouser.com/ds/2/88/941C-559626.pdf. Notice in the data sheet that information about IRMS is given for each part. Even better, this figure is given for 100kHz, which is likely close to what you'll be using.

The current circulating in the capacitors can be much higher than the current coming from the power supply. This is because an LC circuit can store energy. A general rule of thumb is to calculate the impedance of the capacitor at the frequency you intend to use it at, and divide it into the maximum operating voltage across the capacitor. This gives a value for the amperage circulating in the LC circuit. From there, you can refer to the data sheet to determine how many capacitors you need in parallel to keep this part of the circuit from blowing up. Whatever the maximum voltage is across the caps, make sure that their voltage rating is at least double that for safety. I'm engaging in a bit of hand-waving here, but hopefully this provides some help for the capacitor selection.

Good job on the PCB, by the way.

violet sin
International Hazard

Posts: 1357
Registered: 2-9-2012
Location: Back yard staring at stars
Member Is Offline

Mood: Good

I have 10 of the 470KΩ resistors, 20x 4007 fast diodes, 10 IRFP205N, 5x IN5349b zener-d, 2 of those caps ordered almost 2 years ago, and a pile of various bits ripped off boards that weren't new. have a pile of the big microwave caps, at least 6. a number of other much smaller MKP caps/a fist full of several KV range ceramic caps.

then on the way are some
MOSFET IRFP460N x10, IN4742 12V 1W zener x10, IN4767 18V 1W zener x20, IN5822 3A 40V schotkeys x20, for the heck of it considered getting 2x tiny 12v fans, like the size of a US penny,... but 16$free shipping will have to wait would look cool on the green heatsinks http://www.ebay.com/itm/131500008965?_trksid=p2060353.m1438.... I'm hoping to get more time to read on something bigger than my phone... sux only having one page open, reloading any tab every time you swap to another one open, on such a small screen. it makes learning stuff like this FRUSTRATING!!! also my father is a ham operator, and can give some advice, if the concept is similar to his past projects ill get answers. though most my projects bear little resemblance to his. I've come to the conclusion I just need to start an electronics notebook to go with my chem one. much nicer to find last times notes in one spot not peppered with random junk unrelated. I have a number of decent books at my disposal, have to dig them out. many are either WAY to simplified, or over my head. high school electronics was long ago, time to get back to it eh. I really appreciate the help here guys, been trying to do my homework and testing before posting more questions. it's the practical knowledge I want. guess it's time to read up and wait for the mail. thanks Edited in some pics 1)Some of the parts recently ripped off boards. 2)weird diode 3) 3 transformers from the same board, had a pile of 2.2kv ceramic caps too 4) sintered glass diodes, byv76, byw 34-tfk, some with 228-ph end. Kinda cool, haven't seen them often. [Edited on 24-2-2016 by violet sin] woelen Super Administrator Posts: 7582 Registered: 20-8-2005 Location: Netherlands Member Is Offline Mood: interested My ZVS driver never was pushed to the limit. It only has seen 13.8 Volts at input, simply because I have no other sufficiently powerful supply. I found the following on eBay in increasing price: http://www.ebay.nl/itm/390628047656?_trksid=p2060353.m1438.l... http://www.ebay.nl/itm/222014819487?_trksid=p2060353.m1438.l... http://www.ebay.nl/itm/161856625044?_trksid=p2060353.m1438.l... These all are 24 volts units, capable of delivering large currents of 15 ... 20 A. Could these be used safely with the ZVS-driver? These are switched power supplies. My 13.8 V unit is a big and heavy transformer, with a simple 4-diode rectifier, a huge 47000 uF capacitor bank, a handful of big 2N3055 transistors and a LM723 regulator circuit. Very robust old technology, which can withstand quite some abuse. I once made a nice 12 V and 5 V power supply from a PC's ATX power supply: http://woelen.homescience.net/science/chem/misc/psu.html This thing worked very well for electrolysis experiments and was very robust in terms of overloading it with low resistance or even shorting it, but when I did my first high voltage experiments with a small 15 kV DC power supply, salvaged from an old monitor, it quickly died. I did only draw a few hundreds of milliamps from the 12 V terminal. I am afraid that some low power, but high voltage statics destroyed some sensitive CMOS circuit in the power supply. Could this also happen when I want to use the 24 volt unit with switched regulator for my ZVS driver? The art of wondering makes life worth living... Want to wonder? Look at https://woelen.homescience.net IrC International Hazard Posts: 2710 Registered: 7-3-2005 Location: Eureka Member Is Offline Mood: Discovering While yes it is possible you could hurt one with transients from the ZVS I doubt you will have any problems so long as you stay within the current ratings of the supply. You could if concerned build some sort of spike suppressing circuit on the DC input side of the ZVS to help protect the supply but I really doubt you have to worry. "Science is the belief in the ignorance of the experts" Richard Feynman WGTR International Hazard Posts: 948 Registered: 29-9-2013 Location: Online Member Is Offline Mood: Outline  Quote: Originally posted by woelen This thing worked very well for electrolysis experiments and was very robust in terms of overloading it with low resistance or even shorting it, but when I did my first high voltage experiments with a small 15 kV DC power supply, salvaged from an old monitor, it quickly died. I did only draw a few hundreds of milliamps from the 12 V terminal. I am afraid that some low power, but high voltage statics destroyed some sensitive CMOS circuit in the power supply. Could this also happen when I want to use the 24 volt unit with switched regulator for my ZVS driver? I've done it before myself. I was powering a circuit that created high energy transients, and managed to break two expensive power supplies, even though I had the outputs current limited. There were some transistors inside that shorted out; once these were replaced, everything worked fine again (but I didn't use them again for that ill-fated application). If enough high frequency noise makes it back into the power supply, these kinds of things can happen. As IrC mentioned, it's possible to filter out the noise. The exact filter network requirements depend a lot on how fast things are switching, and how much energy is involved. WGTR International Hazard Posts: 948 Registered: 29-9-2013 Location: Online Member Is Offline Mood: Outline Violet sin, it looks like you took apart a UPS. I recognize some of the silicon and magnetics. Those glass diodes are actually pretty useful for high voltage work. They are avalanche diodes, and are designed to survive over-voltage events that would destroy ordinary diodes. Basically, they are like high voltage zener diodes. You can safely stack several of them in series to get higher voltage ratings, like when you're trying to rectify high voltages. IrC International Hazard Posts: 2710 Registered: 7-3-2005 Location: Eureka Member Is Offline Mood: Discovering Forgot to mention woelen but get the largest supply if it is within your budget. Better to have too many potential amps and not need them. You may later scale up some project forcing you to yet again go shopping. Most importantly a supply loafing outlasts one running at the edge, and if you blow it you will now have paid nearly double the cost of the larger supply. Since if the first purchase failed, you must add that loss in money to the price of the larger replacement supply. Far cheaper to pay a little more in the beginning and not need to go shopping later. "Science is the belief in the ignorance of the experts" Richard Feynman violet sin International Hazard Posts: 1357 Registered: 2-9-2012 Location: Back yard staring at stars Member Is Offline Mood: Good not much love from my project just got in some lower watt zeners 12/18v, the right 2W resistors, IFRP460's and some other non related bits. I tried with the correct value resistors, but perhaps some of the components were more damaged than my multimeter led me to believe? no arc's issued forth, no hum of flowing electricity, but no smoke/heat either. all ambient temp. just does NOTHING. ATX PSU isnt dropping dead when connected, measured correct voltage on rail so no Vdroop, quick amperage test showed pleny( and quickly warmed test leads). next up is winding a better inductor with thick wire, looking for better caps, and redesigning my PCB ( the main reason it's unattended ATM ). not that this one is bad, just want a batter parts packing geometry for an easily packaged unit. a guy doesn't need too many 'random bits on board' type projects dumped in a box for use *sometime* in the future. there is a LOT to learn about the various semiconductor parts available... soo much reading. projects on the table now are LED desk lamp(95% done), some sort of power supply to take abuse ( instead of the 70$ ebay unit I love), understanding and attempting to build my own custom LED driver for nightlights.

basically my time now is spent on electronics projects and research, instead of chem. got a note book for documenting the process, starting from small simple units around the house and from ebay. 200W scr dimmer, CFL bulbs, 3w led driver, motion detector light sensor, kids toys etc. sketch the circuit, read, understand and fix if possible. if not you learn stuff. then I will get back to the harder stuff like the stepper driver I failed miserably on.

just easier for me to mess with electronics right now then chem it up at home, and I always went back and forth any way every couple months or so.

funny little side note, I tried to get a spec sheet for an 8-pin BP9011 chip(on the 3x 1W CC LED driver) from an alexpres seller. the part is not listed in any datasheet search engine, assuming it is a generic overseas chip name instead of the proper manufacturer designation. anyway, he quoted me 10$ea for the chips, couldn't provide a spec sheet and said only "if the part number is the same it will work".. meanwhile the whole led driver costs 1-2$ US on ebay with free shipping, LOL . they do have great prices on triac's of considerable power though
Pages:  1  2    4

 Sciencemadness Discussion Board » Fundamentals » Miscellaneous » Dangers/risks of Mazilli ZVS driver? Select A Forum Fundamentals   » Chemistry in General   » Organic Chemistry   » Reagents and Apparatus Acquisition   » Beginnings   » Responsible Practices   » Miscellaneous   » The Wiki Special topics   » Technochemistry   » Energetic Materials   » Biochemistry   » Radiochemistry   » Computational Models and Techniques   » Prepublication Non-chemistry   » Forum Matters   » Legal and Societal Issues